Theorem addcomgi

Description: Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	addcomgi	⊢ ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		addcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
2		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
3	2	fdmi	⊢ dom + = ( ℂ × ℂ )
4	3	ndmovcom	⊢ ( ¬ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
5	1 4	pm2.61i	⊢ ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 )