dvhvaddass

	Ref	Expression
Hypotheses	dvhvaddcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhvaddcl.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dvhvaddcl.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dvhvaddcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvhvaddcl.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
	dvhvaddcl.p	⊢ ⨣ = ( +_g ‘ 𝐷 )
	dvhvaddcl.a	⊢ + = ( +_g ‘ 𝑈 )
Assertion	dvhvaddass	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝐹 + 𝐺 ) + 𝐼 ) = ( 𝐹 + ( 𝐺 + 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvhvaddcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvhvaddcl.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		dvhvaddcl.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4		dvhvaddcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dvhvaddcl.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
6		dvhvaddcl.p	⊢ ⨣ = ( +_g ‘ 𝐷 )
7		dvhvaddcl.a	⊢ + = ( +_g ‘ 𝑈 )
8		coass	⊢ ( ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) )
9	1 2 3 4 5 7 6	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ )
10	9	3adantr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ )
11	10	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝐹 + 𝐺 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ ) )
12		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
13		fvex	⊢ ( 1^st ‘ 𝐺 ) ∈ V
14	12 13	coex	⊢ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) ∈ V
15		ovex	⊢ ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ∈ V
16	14 15	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ ) = ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) )
17	11 16	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝐹 + 𝐺 ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) )
18	17	coeq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1^st ‘ ( 𝐹 + 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) = ( ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) )
19	1 2 3 4 5 7 6	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐺 + 𝐼 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ )
20	19	3adantr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐺 + 𝐼 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ )
21	20	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝐺 + 𝐼 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ ) )
22		fvex	⊢ ( 1^st ‘ 𝐼 ) ∈ V
23	13 22	coex	⊢ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) ∈ V
24		ovex	⊢ ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ∈ V
25	23 24	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ ) = ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) )
26	21 25	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝐺 + 𝐼 ) ) = ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) )
27	26	coeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( 𝐺 + 𝐼 ) ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) ) )
28	8 18 27	3eqtr4a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1^st ‘ ( 𝐹 + 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( 𝐺 + 𝐼 ) ) ) )
29		xp2nd	⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝐹 ) ∈ 𝐸 )
30		xp2nd	⊢ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝐺 ) ∈ 𝐸 )
31		xp2nd	⊢ ( 𝐼 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝐼 ) ∈ 𝐸 )
32	29 30 31	3anim123i	⊢ ( ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) )
33		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
34	1 33 4 5	dvhsca	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
35	1 33	erngdv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
36	34 35	eqeltrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ DivRing )
37		drnggrp	⊢ ( 𝐷 ∈ DivRing → 𝐷 ∈ Grp )
38	36 37	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Grp )
39	38	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → 𝐷 ∈ Grp )
40		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( 2^nd ‘ 𝐹 ) ∈ 𝐸 )
41		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
42	1 3 4 5 41	dvhbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
43	42	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( Base ‘ 𝐷 ) = 𝐸 )
44	40 43	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( 2^nd ‘ 𝐹 ) ∈ ( Base ‘ 𝐷 ) )
45		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( 2^nd ‘ 𝐺 ) ∈ 𝐸 )
46	45 43	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( 2^nd ‘ 𝐺 ) ∈ ( Base ‘ 𝐷 ) )
47		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( 2^nd ‘ 𝐼 ) ∈ 𝐸 )
48	47 43	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( 2^nd ‘ 𝐼 ) ∈ ( Base ‘ 𝐷 ) )
49	41 6	grpass	⊢ ( ( 𝐷 ∈ Grp ∧ ( ( 2^nd ‘ 𝐹 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ 𝐺 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ 𝐼 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ) )
50	39 44 46 48 49	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2^nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐺 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝐼 ) ∈ 𝐸 ) ) → ( ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ) )
51	32 50	sylan2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ) )
52	10	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ ) )
53	14 15	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⟩ ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) )
54	52 53	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) )
55	54	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) = ( ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) )
56	20	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ ) )
57	23 24	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ ) = ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) )
58	56 57	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) = ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) )
59	58	oveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( ( 2^nd ‘ 𝐺 ) ⨣ ( 2^nd ‘ 𝐼 ) ) ) )
60	51 55 59	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) = ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) ) )
61	28 60	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 1^st ‘ ( 𝐹 + 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( 𝐺 + 𝐼 ) ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) ) ⟩ )
62		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
63	1 2 3 4 5 6 7	dvhvaddcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) ∈ ( 𝑇 × 𝐸 ) )
64	63	3adantr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) ∈ ( 𝑇 × 𝐸 ) )
65		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐼 ∈ ( 𝑇 × 𝐸 ) )
66	1 2 3 4 5 7 6	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐹 + 𝐺 ) ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝐹 + 𝐺 ) + 𝐼 ) = ⟨ ( ( 1^st ‘ ( 𝐹 + 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ )
67	62 64 65 66	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝐹 + 𝐺 ) + 𝐼 ) = ⟨ ( ( 1^st ‘ ( 𝐹 + 𝐺 ) ) ∘ ( 1^st ‘ 𝐼 ) ) , ( ( 2^nd ‘ ( 𝐹 + 𝐺 ) ) ⨣ ( 2^nd ‘ 𝐼 ) ) ⟩ )
68		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐹 ∈ ( 𝑇 × 𝐸 ) )
69	1 2 3 4 5 6 7	dvhvaddcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐺 + 𝐼 ) ∈ ( 𝑇 × 𝐸 ) )
70	69	3adantr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐺 + 𝐼 ) ∈ ( 𝑇 × 𝐸 ) )
71	1 2 3 4 5 7 6	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝐺 + 𝐼 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + ( 𝐺 + 𝐼 ) ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( 𝐺 + 𝐼 ) ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) ) ⟩ )
72	62 68 70 71	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + ( 𝐺 + 𝐼 ) ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( 𝐺 + 𝐼 ) ) ) , ( ( 2^nd ‘ 𝐹 ) ⨣ ( 2^nd ‘ ( 𝐺 + 𝐼 ) ) ) ⟩ )
73	61 67 72	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐼 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝐹 + 𝐺 ) + 𝐼 ) = ( 𝐹 + ( 𝐺 + 𝐼 ) ) )

Metamath Proof Explorer

Theorem dvhvaddass

Proof