Theorem rmul_expand_add_add

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ d ∈ ℝ, hypo.
05. 1, 2 ⊢ a + b ∈ ℝ, radd_closed 1 2.
06. 1, 2, 3, 4 ⊢ (a + b)⋅(c + d) = (a + b)⋅c + (a + b)⋅d,
  rmul_distl_add 5 3 4.
07. 1, 2, 3 ⊢ (a + b)⋅c = a⋅c + b⋅c, rmul_distr_add 1 2 3.
08. 1, 2, 4 ⊢ (a + b)⋅d = a⋅d + b⋅d, rmul_distr_add 1 2 4.
09. 1, 2, 3, 4 ⊢ (a + b)⋅c + (a + b)⋅d =
  a⋅c + b⋅c + (a⋅d + b⋅d), eq_cong_ii 7 8, f x y = x + y.
10. 1, 2, 3, 4 ⊢ (a + b)⋅(c + d) = a⋅c + b⋅c + (a⋅d + b⋅d),
  eq_trans 6 9.
11. 1, 3 ⊢ a⋅c ∈ ℝ, rmul_closed 1 3.
12. 2, 3 ⊢ b⋅c ∈ ℝ, rmul_closed 2 3.
13. 1, 4 ⊢ a⋅d ∈ ℝ, rmul_closed 1 4.
14. 2, 4 ⊢ b⋅d ∈ ℝ, rmul_closed 2 4.
15. 1, 2, 3 ⊢ a⋅c + b⋅c ∈ ℝ, radd_closed 11 12.
16. 1, 2, 3, 4 ⊢ a⋅c + b⋅c + a⋅d + b⋅d = a⋅c + b⋅c + (a⋅d + b⋅d),
  radd_assoc 15 13 14.
17. 1, 2, 3, 4 ⊢ (a + b)⋅(c + d) = a⋅c + b⋅c + a⋅d + b⋅d,
  eq_trans_rr 10 16.
rmul_expand_add_add. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ →
  (a + b)⋅(c + d) = a⋅c + b⋅c + a⋅d + b⋅d, subj_intro_iv 17.

Dependencies
The given proof depends on seven axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, rmul_closed, rmul_comm, rmul_distl_add.