dvhvaddass

	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	dvhvaddass	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to (F \underset{˙}{+} G) \underset{˙}{+} I = F \underset{˙}{+} (G \underset{˙}{+} I)$

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		coass	$⊢ (1^{st} (F) \circ 1^{st} (G)) \circ 1^{st} (I) = 1^{st} (F) \circ (1^{st} (G) \circ 1^{st} (I))$
9	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)⟩$
10	9	3adantr3	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to F \underset{˙}{+} G = ⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩$
11	10	fveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (F \underset{˙}{+} G) = 1^{st} (⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩)$
12		fvex	$⊢ 1^{st} (F) \in V$
13		fvex	$⊢ 1^{st} (G) \in V$
14	12 13	coex	$⊢ 1^{st} (F) \circ 1^{st} (G) \in V$
15		ovex	$⊢ 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G) \in V$
16	14 15	op1st	$⊢ 1^{st} (⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩) = 1^{st} (F) \circ 1^{st} (G)$
17	11 16	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (F \underset{˙}{+} G) = 1^{st} (F) \circ 1^{st} (G)$
18	17	coeq1d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (F \underset{˙}{+} G) \circ 1^{st} (I) = (1^{st} (F) \circ 1^{st} (G)) \circ 1^{st} (I)$
19	1 2 3 4 5 7 6	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (G \in (T \times E) \land I \in (T \times E))) \to G \underset{˙}{+} I = ⟨1^{st} (G) \circ 1^{st} (I), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)⟩$
20	19	3adantr1	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to G \underset{˙}{+} I = ⟨1^{st} (G) \circ 1^{st} (I), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)⟩$
21	20	fveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (G \underset{˙}{+} I) = 1^{st} (⟨1^{st} (G) \circ 1^{st} (I), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)⟩)$
22		fvex	$⊢ 1^{st} (I) \in V$
23	13 22	coex	$⊢ 1^{st} (G) \circ 1^{st} (I) \in V$
24		ovex	$⊢ 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I) \in V$
25	23 24	op1st	$⊢ 1^{st} (⟨1^{st} (G) \circ 1^{st} (I), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)⟩) = 1^{st} (G) \circ 1^{st} (I)$
26	21 25	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (G \underset{˙}{+} I) = 1^{st} (G) \circ 1^{st} (I)$
27	26	coeq2d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (F) \circ 1^{st} (G \underset{˙}{+} I) = 1^{st} (F) \circ (1^{st} (G) \circ 1^{st} (I))$
28	8 18 27	3eqtr4a	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 1^{st} (F \underset{˙}{+} G) \circ 1^{st} (I) = 1^{st} (F) \circ 1^{st} (G \underset{˙}{+} I)$
29		xp2nd	$⊢ F \in (T \times E) \to 2^{nd} (F) \in E$
30		xp2nd	$⊢ G \in (T \times E) \to 2^{nd} (G) \in E$
31		xp2nd	$⊢ I \in (T \times E) \to 2^{nd} (I) \in E$
32	29 30 31	3anim123i	$⊢ (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E)) \to (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)$
33		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
34	1 33 4 5	dvhsca	$⊢ (K \in HL \land W \in H) \to D = EDRing (K) (W)$
35	1 33	erngdv	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in DivRing$
36	34 35	eqeltrd	$⊢ (K \in HL \land W \in H) \to D \in DivRing$
37		drnggrp	$⊢ D \in DivRing \to D \in Grp$
38	36 37	syl	$⊢ (K \in HL \land W \in H) \to D \in Grp$
39	38	adantr	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to D \in Grp$
40		simpr1	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to 2^{nd} (F) \in E$
41		eqid	$⊢ {Base}_{D} = {Base}_{D}$
42	1 3 4 5 41	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{D} = E$
43	42	adantr	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to {Base}_{D} = E$
44	40 43	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to 2^{nd} (F) \in {Base}_{D}$
45		simpr2	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to 2^{nd} (G) \in E$
46	45 43	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to 2^{nd} (G) \in {Base}_{D}$
47		simpr3	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to 2^{nd} (I) \in E$
48	47 43	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to 2^{nd} (I) \in {Base}_{D}$
49	41 6	grpass	$⊢ (D \in Grp \land (2^{nd} (F) \in {Base}_{D} \land 2^{nd} (G) \in {Base}_{D} \land 2^{nd} (I) \in {Base}_{D})) \to (2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)) \underset{˙}{⨣} 2^{nd} (I) = 2^{nd} (F) \underset{˙}{⨣} (2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I))$
50	39 44 46 48 49	syl13anc	$⊢ ((K \in HL \land W \in H) \land (2^{nd} (F) \in E \land 2^{nd} (G) \in E \land 2^{nd} (I) \in E)) \to (2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)) \underset{˙}{⨣} 2^{nd} (I) = 2^{nd} (F) \underset{˙}{⨣} (2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I))$
51	32 50	sylan2	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to (2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)) \underset{˙}{⨣} 2^{nd} (I) = 2^{nd} (F) \underset{˙}{⨣} (2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I))$
52	10	fveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (F \underset{˙}{+} G) = 2^{nd} (⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩)$
53	14 15	op2nd	$⊢ 2^{nd} (⟨1^{st} (F) \circ 1^{st} (G), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)⟩) = 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)$
54	52 53	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (F \underset{˙}{+} G) = 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)$
55	54	oveq1d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (F \underset{˙}{+} G) \underset{˙}{⨣} 2^{nd} (I) = (2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G)) \underset{˙}{⨣} 2^{nd} (I)$
56	20	fveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (G \underset{˙}{+} I) = 2^{nd} (⟨1^{st} (G) \circ 1^{st} (I), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)⟩)$
57	23 24	op2nd	$⊢ 2^{nd} (⟨1^{st} (G) \circ 1^{st} (I), 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)⟩) = 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)$
58	56 57	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (G \underset{˙}{+} I) = 2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I)$
59	58	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G \underset{˙}{+} I) = 2^{nd} (F) \underset{˙}{⨣} (2^{nd} (G) \underset{˙}{⨣} 2^{nd} (I))$
60	51 55 59	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to 2^{nd} (F \underset{˙}{+} G) \underset{˙}{⨣} 2^{nd} (I) = 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G \underset{˙}{+} I)$
61	28 60	opeq12d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to ⟨1^{st} (F \underset{˙}{+} G) \circ 1^{st} (I), 2^{nd} (F \underset{˙}{+} G) \underset{˙}{⨣} 2^{nd} (I)⟩ = ⟨1^{st} (F) \circ 1^{st} (G \underset{˙}{+} I), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G \underset{˙}{+} I)⟩$
62		simpl	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to (K \in HL \land W \in H)$
63	1 2 3 4 5 6 7	dvhvaddcl	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E))) \to F \underset{˙}{+} G \in (T \times E)$
64	63	3adantr3	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to F \underset{˙}{+} G \in (T \times E)$
65		simpr3	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to I \in (T \times E)$
66	1 2 3 4 5 7 6	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (F \underset{˙}{+} G \in (T \times E) \land I \in (T \times E))) \to (F \underset{˙}{+} G) \underset{˙}{+} I = ⟨1^{st} (F \underset{˙}{+} G) \circ 1^{st} (I), 2^{nd} (F \underset{˙}{+} G) \underset{˙}{⨣} 2^{nd} (I)⟩$
67	62 64 65 66	syl12anc	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to (F \underset{˙}{+} G) \underset{˙}{+} I = ⟨1^{st} (F \underset{˙}{+} G) \circ 1^{st} (I), 2^{nd} (F \underset{˙}{+} G) \underset{˙}{⨣} 2^{nd} (I)⟩$
68		simpr1	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to F \in (T \times E)$
69	1 2 3 4 5 6 7	dvhvaddcl	$⊢ ((K \in HL \land W \in H) \land (G \in (T \times E) \land I \in (T \times E))) \to G \underset{˙}{+} I \in (T \times E)$
70	69	3adantr1	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to G \underset{˙}{+} I \in (T \times E)$
71	1 2 3 4 5 7 6	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \underset{˙}{+} I \in (T \times E))) \to F \underset{˙}{+} (G \underset{˙}{+} I) = ⟨1^{st} (F) \circ 1^{st} (G \underset{˙}{+} I), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G \underset{˙}{+} I)⟩$
72	62 68 70 71	syl12anc	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to F \underset{˙}{+} (G \underset{˙}{+} I) = ⟨1^{st} (F) \circ 1^{st} (G \underset{˙}{+} I), 2^{nd} (F) \underset{˙}{⨣} 2^{nd} (G \underset{˙}{+} I)⟩$
73	61 67 72	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in (T \times E) \land G \in (T \times E) \land I \in (T \times E))) \to (F \underset{˙}{+} G) \underset{˙}{+} I = F \underset{˙}{+} (G \underset{˙}{+} I)$

Metamath Proof Explorer

Theorem dvhvaddass

Proof