Theorem addrcom

Description: Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012)

	Ref	Expression
Assertion	addrcom	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +𝑟 𝐵 ) = ( 𝐵 +𝑟 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		addrfn	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +𝑟 𝐵 ) Fn ℝ )
2		addrfn	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐵 +𝑟 𝐴 ) Fn ℝ )
3	2	ancoms	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐵 +𝑟 𝐴 ) Fn ℝ )
4		addcomgi	⊢ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) = ( ( 𝐵 ‘ 𝑥 ) + ( 𝐴 ‘ 𝑥 ) )
5		addrfv	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 +𝑟 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) )
6		addrfv	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 +𝑟 𝐴 ) ‘ 𝑥 ) = ( ( 𝐵 ‘ 𝑥 ) + ( 𝐴 ‘ 𝑥 ) ) )
7	6	3com12	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 +𝑟 𝐴 ) ‘ 𝑥 ) = ( ( 𝐵 ‘ 𝑥 ) + ( 𝐴 ‘ 𝑥 ) ) )
8	4 5 7	3eqtr4a	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 +𝑟 𝐵 ) ‘ 𝑥 ) = ( ( 𝐵 +𝑟 𝐴 ) ‘ 𝑥 ) )
9	8	3expia	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝑥 ∈ ℝ → ( ( 𝐴 +𝑟 𝐵 ) ‘ 𝑥 ) = ( ( 𝐵 +𝑟 𝐴 ) ‘ 𝑥 ) ) )
10	9	ralrimiv	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ∀ 𝑥 ∈ ℝ ( ( 𝐴 +𝑟 𝐵 ) ‘ 𝑥 ) = ( ( 𝐵 +𝑟 𝐴 ) ‘ 𝑥 ) )
11		eqfnfv	⊢ ( ( ( 𝐴 +𝑟 𝐵 ) Fn ℝ ∧ ( 𝐵 +𝑟 𝐴 ) Fn ℝ ) → ( ( 𝐴 +𝑟 𝐵 ) = ( 𝐵 +𝑟 𝐴 ) ↔ ∀ 𝑥 ∈ ℝ ( ( 𝐴 +𝑟 𝐵 ) ‘ 𝑥 ) = ( ( 𝐵 +𝑟 𝐴 ) ‘ 𝑥 ) ) )
12	10 11	syl5ibrcom	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( ( 𝐴 +𝑟 𝐵 ) Fn ℝ ∧ ( 𝐵 +𝑟 𝐴 ) Fn ℝ ) → ( 𝐴 +𝑟 𝐵 ) = ( 𝐵 +𝑟 𝐴 ) ) )
13	1 3 12	mp2and	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +𝑟 𝐵 ) = ( 𝐵 +𝑟 𝐴 ) )