Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 1, 2 ⊢ -(b⋅a) = b⋅(-a), rmul_compatr_neg 2 1. 04. 1, 2 ⊢ b⋅a = a⋅b, rmul_comm 2 1. 05. 1, 2 ⊢ -(a⋅b) = b⋅(-a), eq_subst 4 3, P t ↔ -t = b⋅(-a). 06. 1 ⊢ (-a) ∈ ℝ, rneg_closed 1. 07. 1, 2 ⊢ b⋅(-a) = (-a)⋅b, rmul_comm 2 6. 08. 1, 2 ⊢ -(a⋅b) = (-a)⋅b, eq_trans 5 7. rmul_compatl_neg. ⊢ a ∈ ℝ → b ∈ ℝ → -(a⋅b) = (-a)⋅b, subj_intro_ii 8.
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.