addrcom

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

		Ref	Expression
	Assertion	addrcom	$⊢ (A \in C \land B \in D) \to A +_{r} B = B +_{r} A$

Step	Hyp	Ref	Expression
1		addrfn	$⊢ (A \in C \land B \in D) \to (A +_{r} B) Fn ℝ$
2		addrfn	$⊢ (B \in D \land A \in C) \to (B +_{r} A) Fn ℝ$
3	2	ancoms	$⊢ (A \in C \land B \in D) \to (B +_{r} A) Fn ℝ$
4		addcomgi	$⊢ A (x) + B (x) = B (x) + A (x)$
5		addrfv	$⊢ (A \in C \land B \in D \land x \in ℝ) \to (A +_{r} B) (x) = A (x) + B (x)$
6		addrfv	$⊢ (B \in D \land A \in C \land x \in ℝ) \to (B +_{r} A) (x) = B (x) + A (x)$
7	6	3com12	$⊢ (A \in C \land B \in D \land x \in ℝ) \to (B +_{r} A) (x) = B (x) + A (x)$
8	4 5 7	3eqtr4a	$⊢ (A \in C \land B \in D \land x \in ℝ) \to (A +_{r} B) (x) = (B +_{r} A) (x)$
9	8	3expia	$⊢ (A \in C \land B \in D) \to (x \in ℝ \to (A +_{r} B) (x) = (B +_{r} A) (x))$
10	9	ralrimiv	$⊢ (A \in C \land B \in D) \to \forall x \in ℝ (A +_{r} B) (x) = (B +_{r} A) (x)$
11		eqfnfv	$⊢ ((A +_{r} B) Fn ℝ \land (B +_{r} A) Fn ℝ) \to (A +_{r} B = B +_{r} A \leftrightarrow \forall x \in ℝ (A +_{r} B) (x) = (B +_{r} A) (x))$
12	10 11	syl5ibrcom	$⊢ (A \in C \land B \in D) \to (((A +_{r} B) Fn ℝ \land (B +_{r} A) Fn ℝ) \to A +_{r} B = B +_{r} A)$
13	1 3 12	mp2and	$⊢ (A \in C \land B \in D) \to A +_{r} B = B +_{r} A$

Metamath Proof Explorer