Theorem rmul_distl_sub

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. ⊢ b - c = b + (-c), rsub_eq.
05. ⊢ a⋅(b - c) = a⋅(b + (-c)), eq_cong 4, f x = a⋅x.
06. 3 ⊢ -c ∈ ℝ, rneg_closed 3.
07. 1, 2, 3 ⊢ a⋅(b + (-c)) = a⋅b + a⋅(-c),
  rmul_distl_add 1 2 6.
08. 1, 2, 3 ⊢ a⋅(b - c) = a⋅b + a⋅(-c), eq_trans 5 7.
09. 1, 3 ⊢ -(a⋅c) = a⋅(-c), rmul_compatr_neg 1 3.
10. 1, 2, 3 ⊢ a⋅(b - c) = a⋅b + -(a⋅c),
  eq_subst_rev 9 8, P t ↔ a⋅(b - c) = a⋅b + t.
11. ⊢ a⋅b - a⋅c = a⋅b + -(a⋅c), rsub_eq.
12. ⊢ a⋅b + -(a⋅c) = a⋅b - a⋅c, eq_symm 11.
13. 1, 2, 3 ⊢ a⋅(b - c) = a⋅b - a⋅c, eq_trans 10 12.
rmul_distl_sub. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a⋅(b - c) = a⋅b - a⋅c, subj_intro_iii 13.

Dependencies
The given proof depends on 10 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_distl_add, rneg_closed.