dvhvaddcomN

Description: Commutativity of vector sum. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvhvaddcl.h	$⊢ H = LHyp (K)$
	dvhvaddcl.t	$⊢ T = LTrn (K) (W)$
	dvhvaddcl.e	$⊢ E = TEndo (K) (W)$
	dvhvaddcl.u	$⊢ U = DVecH (K) (W)$
	dvhvaddcl.d	$⊢ D = Scalar (U)$
	dvhvaddcl.p	$⊢ \underset{˙}{⨣} = +_{D}$
	dvhvaddcl.a	$⊢ \underset{˙}{+} = +_{U}$
Assertion	dvhvaddcomN	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to F \underset{˙}{+} G = G \underset{˙}{+} F$

Proof

Step	Hyp	Ref	Expression
1		dvhvaddcl.h	$⊢ H = LHyp (K)$
2		dvhvaddcl.t	$⊢ T = LTrn (K) (W)$
3		dvhvaddcl.e	$⊢ E = TEndo (K) (W)$
4		dvhvaddcl.u	$⊢ U = DVecH (K) (W)$
5		dvhvaddcl.d	$⊢ D = Scalar (U)$
6		dvhvaddcl.p	$⊢ \underset{˙}{⨣} = +_{D}$
7		dvhvaddcl.a	$⊢ \underset{˙}{+} = +_{U}$
8		simpl	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to (K \in HL \land W \in H)$
9		xp1st	$⊢ F \in (T \times E) \to 1^{st} (F) \in T$
10	9	ad2antrl	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 1^{st} (F) \in T$
11		xp1st	$⊢ G \in (T \times E) \to 1^{st} (G) \in T$
12	11	ad2antll	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 1^{st} (G) \in T$
13	1 2	ltrncom	$⊢ ((K \in HL \land W \in H) \land 1^{st} (F) \in T \land 1^{st} (G) \in T) \to 1^{st} (F) \circ 1^{st} (G) = 1^{st} (G) \circ 1^{st} (F)$
14	8 10 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 1^{st} (F) \circ 1^{st} (G) = 1^{st} (G) \circ 1^{st} (F)$
15		xp2nd	$⊢ F \in (T \times E) \to 2^{nd} (F) \in E$
16		xp2nd	$⊢ G \in (T \times E) \to 2^{nd} (G) \in E$
17	15 16	anim12i	$⊢ (F \in (T \times E) \land G \in (T \times E)) \to (2^{nd} (F) \in E \land 2^{nd} (G) \in E)$
18		eqid	$⊢ (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) = (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c)))$
19	1 2 3 18	tendoplcom	$⊢ ((K \in HL \land W \in H) \land 2^{nd} (F) \in E \land 2^{nd} (G) \in E) \to 2^{nd} (F) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (G) = 2^{nd} (G) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (F)$
20	19	3expb	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E)) \to 2^{nd} (F) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (G) = 2^{nd} (G) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (F)$
21	17 20	sylan2	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 2^{nd} (F) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (G) = 2^{nd} (G) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (F)$
22	1 2 3 4 5 18 6	dvhfplusr	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⨣} = (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c)))$
23	22	adantr	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to \underset{˙}{⨣} = (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c)))$
24	23	oveqd	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G) = 2^{nd} (F) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (G)$
25	23	oveqd	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (F) = 2^{nd} (G) (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c))) 2^{nd} (F)$
26	21 24 25	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G) = 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (F)$
27	14 26	opeq12d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩ = ⟨1^{st} (G) \circ 1^{st} (F), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (F)⟩$
28	1 2 3 4 5 7 6	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to F \underset{˙}{+} G = ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩$
29	1 2 3 4 5 7 6	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (G \in (T \times E) \land F \in (T \times E))) \to G \underset{˙}{+} F = ⟨1^{st} (G) \circ 1^{st} (F), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (F)⟩$
30	29	ancom2s	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to G \underset{˙}{+} F = ⟨1^{st} (G) \circ 1^{st} (F), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (F)⟩$
31	27 28 30	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to F \underset{˙}{+} G = G \underset{˙}{+} F$

Metamath Proof Explorer

Theorem dvhvaddcomN

Proof