Theorem rmul_distr_sub

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 1, 2 ⊢ a - b ∈ ℝ, rsub_closed 1 2.
05. 1, 2, 3 ⊢ (a - b)⋅c = c⋅(a - b), rmul_comm 4 3.
06. 1, 2, 3 ⊢ c⋅(a - b) = c⋅a - c⋅b, rmul_distl_sub 3 1 2.
07. 1, 3 ⊢ c⋅a = a⋅c, rmul_comm 3 1.
08. 2, 3 ⊢ c⋅b = b⋅c, rmul_comm 3 2.
09. 1, 3 ⊢ c⋅a - c⋅b = a⋅c - c⋅b, eq_cong 7, f t = t - c⋅b.
10. 1, 2, 3 ⊢ c⋅a - c⋅b = a⋅c - b⋅c, eq_subst 8 9,
  P t ↔ c⋅a - c⋅b = a⋅c - t.
11. 1, 2, 3 ⊢ (a - b)⋅c = c⋅a - c⋅b, eq_trans 5 6.
12. 1, 2, 3 ⊢ (a - b)⋅c = a⋅c - b⋅c, eq_trans 11 10.
rmul_distr_sub. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  (a - b)⋅c = a⋅c - b⋅c, subj_intro_iii 12.

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