dvhlveclem

Description: Lemma for dvhlvec . TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does ph -> method shorten proof? (Contributed by NM, 22-Oct-2013) (Proof shortened by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	dvhgrp.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dvhgrp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhgrp.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dvhgrp.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dvhgrp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvhgrp.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
	dvhgrp.p	⊢ ⨣ = ( +_g ‘ 𝐷 )
	dvhgrp.a	⊢ + = ( +_g ‘ 𝑈 )
	dvhgrp.o	⊢ 0 = ( 0_g ‘ 𝐷 )
	dvhgrp.i	⊢ 𝐼 = ( inv_g ‘ 𝐷 )
	dvhlvec.m	⊢ × = ( ._r ‘ 𝐷 )
	dvhlvec.s	⊢ · = ( ·_𝑠 ‘ 𝑈 )
Assertion	dvhlveclem	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		dvhgrp.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dvhgrp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dvhgrp.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dvhgrp.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5		dvhgrp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		dvhgrp.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
7		dvhgrp.p	⊢ ⨣ = ( +_g ‘ 𝐷 )
8		dvhgrp.a	⊢ + = ( +_g ‘ 𝑈 )
9		dvhgrp.o	⊢ 0 = ( 0_g ‘ 𝐷 )
10		dvhgrp.i	⊢ 𝐼 = ( inv_g ‘ 𝐷 )
11		dvhlvec.m	⊢ × = ( ._r ‘ 𝐷 )
12		dvhlvec.s	⊢ · = ( ·_𝑠 ‘ 𝑈 )
13		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
14	2 3 4 5 13	dvhvbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( 𝑇 × 𝐸 ) )
15	14	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑇 × 𝐸 ) = ( Base ‘ 𝑈 ) )
16	8	a1i	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ( +_g ‘ 𝑈 ) )
17	6	a1i	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( Scalar ‘ 𝑈 ) )
18	12	a1i	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → · = ( ·_𝑠 ‘ 𝑈 ) )
19		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
20	2 4 5 6 19	dvhbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
21	20	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) )
22	7	a1i	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( +_g ‘ 𝐷 ) )
23	11	a1i	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → × = ( ._r ‘ 𝐷 ) )
24		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
25	2 24 5 6	dvhsca	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
26	25	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1_r ‘ 𝐷 ) = ( 1_r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
27		eqid	⊢ ( 1_r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 1_r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
28	2 3 24 27	erng1r	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1_r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( I ↾ 𝑇 ) )
29	26 28	eqtr2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) = ( 1_r ‘ 𝐷 ) )
30	2 24	erngdv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
31	25 30	eqeltrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ DivRing )
32		drngring	⊢ ( 𝐷 ∈ DivRing → 𝐷 ∈ Ring )
33	31 32	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )
34	1 2 3 4 5 6 7 8 9 10	dvhgrp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ Grp )
35	2 3 4 5 12	dvhvscacl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) )
36	35	3impb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) )
37		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
38		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ 𝐸 )
39		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ ( 𝑇 × 𝐸 ) )
40		xp1st	⊢ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) → ( 1^st ‘ 𝑡 ) ∈ 𝑇 )
41	39 40	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ 𝑡 ) ∈ 𝑇 )
42		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑓 ∈ ( 𝑇 × 𝐸 ) )
43		xp1st	⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
44	42 43	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
45	2 3 4	tendospdi1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 1^st ‘ 𝑡 ) ∈ 𝑇 ∧ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ) ) → ( 𝑠 ‘ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ) )
46	37 38 41 44 45	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ) )
47	2 3 4 5 6 8 7	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) = ⟨ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ )
48	47	3adantr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) = ⟨ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ )
49	48	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑡 + 𝑓 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
50		fvex	⊢ ( 1^st ‘ 𝑡 ) ∈ V
51		fvex	⊢ ( 1^st ‘ 𝑓 ) ∈ V
52	50 51	coex	⊢ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) ∈ V
53		ovex	⊢ ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ∈ V
54	52 53	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) )
55	49 54	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑡 + 𝑓 ) ) = ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) )
56	55	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( 1^st ‘ ( 𝑡 + 𝑓 ) ) ) = ( 𝑠 ‘ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) ) )
57	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⟩ )
58	57	3adantr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⟩ )
59	58	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑠 · 𝑡 ) ) = ( 1^st ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) )
60		fvex	⊢ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) ∈ V
61		vex	⊢ 𝑠 ∈ V
62		fvex	⊢ ( 2^nd ‘ 𝑡 ) ∈ V
63	61 62	coex	⊢ ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ∈ V
64	60 63	op1st	⊢ ( 1^st ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) )
65	59 64	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑠 · 𝑡 ) ) = ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) )
66	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
67	66	3adantr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
68	67	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑠 · 𝑓 ) ) = ( 1^st ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
69		fvex	⊢ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ∈ V
70		fvex	⊢ ( 2^nd ‘ 𝑓 ) ∈ V
71	61 70	coex	⊢ ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ∈ V
72	69 71	op1st	⊢ ( 1^st ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) )
73	68 72	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) )
74	65 73	coeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1^st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ) )
75	46 56 74	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( 1^st ‘ ( 𝑡 + 𝑓 ) ) ) = ( ( 1^st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ) )
76	33	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐷 ∈ Ring )
77	21	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) )
78	38 77	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐷 ) )
79		xp2nd	⊢ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝑡 ) ∈ 𝐸 )
80	39 79	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ 𝑡 ) ∈ 𝐸 )
81	80 77	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) )
82		xp2nd	⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝑓 ) ∈ 𝐸 )
83	42 82	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ 𝐸 )
84	83 77	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) )
85	19 7 11	ringdi	⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑠 × ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) = ( ( 𝑠 × ( 2^nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) ) )
86	76 78 81 84 85	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) = ( ( 𝑠 × ( 2^nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) ) )
87	19 7	ringacl	⊢ ( ( 𝐷 ∈ Ring ∧ ( 2^nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) )
88	76 81 84 87	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) )
89	88 77	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 )
90	2 3 4 5 6 11	dvhmulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 ) ) → ( 𝑠 × ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) )
91	37 38 89 90	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) )
92	2 3 4 5 6 11	dvhmulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 2^nd ‘ 𝑡 ) ∈ 𝐸 ) ) → ( 𝑠 × ( 2^nd ‘ 𝑡 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) )
93	37 38 80 92	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2^nd ‘ 𝑡 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) )
94	2 3 4 5 6 11	dvhmulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 2^nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) )
95	37 38 83 94	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) )
96	93 95	oveq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × ( 2^nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
97	86 91 96	3eqtr3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
98	48	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
99	52 53	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑡 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) )
100	98 99	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) = ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) )
101	100	coeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2^nd ‘ 𝑡 ) ⨣ ( 2^nd ‘ 𝑓 ) ) ) )
102	58	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) = ( 2^nd ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) )
103	60 63	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) )
104	102 103	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) )
105	67	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) = ( 2^nd ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
106	69 71	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) )
107	105 106	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) )
108	104 107	oveq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2^nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
109	97 101 108	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) ) = ( ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ) )
110	75 109	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( 𝑠 ‘ ( 1^st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) ) ⟩ = ⟨ ( ( 1^st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ) ⟩ )
111	2 3 4 5 6 7 8	dvhvaddcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
112	111	3adantr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
113	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) ) ⟩ )
114	37 38 112 113	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2^nd ‘ ( 𝑡 + 𝑓 ) ) ) ⟩ )
115	35	3adantr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) )
116	2 3 4 5 12	dvhvscacl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
117	116	3adantr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
118	2 3 4 5 6 8 7	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = ⟨ ( ( 1^st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ) ⟩ )
119	37 115 117 118	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = ⟨ ( ( 1^st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2^nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ) ⟩ )
120	110 114 119	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) )
121		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
122		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ 𝐸 )
123		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ 𝐸 )
124		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑓 ∈ ( 𝑇 × 𝐸 ) )
125	124 43	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
126		eqid	⊢ ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
127	2 3 4 24 126	erngplus2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ) ) → ( ( 𝑠 ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) )
128	121 122 123 125 127	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) )
129	25	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +_g ‘ 𝐷 ) = ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
130	7 129	eqtrid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
131	130	oveqd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 ⨣ 𝑡 ) = ( 𝑠 ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) )
132	131	fveq1d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( ( 𝑠 ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) )
133	132	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( ( 𝑠 ( +_g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) )
134	66	3adantr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
135	134	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑠 · 𝑓 ) ) = ( 1^st ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
136	135 72	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) )
137	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) = ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
138	137	3adantr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) = ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
139	138	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑡 · 𝑓 ) ) = ( 1^st ‘ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
140		fvex	⊢ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ∈ V
141		vex	⊢ 𝑡 ∈ V
142	141 70	coex	⊢ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ∈ V
143	140 142	op1st	⊢ ( 1^st ‘ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) )
144	139 143	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1^st ‘ ( 𝑡 · 𝑓 ) ) = ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) )
145	136 144	coeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1^st ‘ ( 𝑡 · 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) )
146	128 133 145	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1^st ‘ ( 𝑡 · 𝑓 ) ) ) )
147	33	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐷 ∈ Ring )
148	21	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) )
149	122 148	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐷 ) )
150	123 148	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ ( Base ‘ 𝐷 ) )
151	124 82	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ 𝐸 )
152	151 148	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) )
153	19 7 11	ringdir	⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ 𝑡 ∈ ( Base ‘ 𝐷 ) ∧ ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2^nd ‘ 𝑓 ) ) = ( ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2^nd ‘ 𝑓 ) ) ) )
154	147 149 150 152 153	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2^nd ‘ 𝑓 ) ) = ( ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2^nd ‘ 𝑓 ) ) ) )
155	19 7	ringacl	⊢ ( ( 𝐷 ∈ Ring ∧ 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ 𝑡 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑠 ⨣ 𝑡 ) ∈ ( Base ‘ 𝐷 ) )
156	147 149 150 155	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ⨣ 𝑡 ) ∈ ( Base ‘ 𝐷 ) )
157	156 148	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 )
158	2 3 4 5 6 11	dvhmulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ∧ ( 2^nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2^nd ‘ 𝑓 ) ) = ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) )
159	121 157 151 158	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2^nd ‘ 𝑓 ) ) = ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) )
160	121 122 151 94	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) )
161	2 3 4 5 6 11	dvhmulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 2^nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( 𝑡 × ( 2^nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) )
162	121 123 151 161	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 × ( 2^nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) )
163	160 162	oveq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × ( 2^nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2^nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
164	154 159 163	3eqtr3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) = ( ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
165	134	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) = ( 2^nd ‘ ⟨ ( 𝑠 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
166	165 106	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) )
167	138	fveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) = ( 2^nd ‘ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
168	140 142	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) )
169	167 168	eqtrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) = ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) )
170	166 169	oveq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
171	164 170	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) = ( ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) ) )
172	146 171	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1^st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) ) ⟩ )
173	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
174	121 157 124 173	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
175	116	3adantr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
176	2 3 4 5 12	dvhvscacl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
177	176	3adantr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
178	2 3 4 5 6 8 7	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = ⟨ ( ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1^st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) ) ⟩ )
179	121 175 177 178	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = ⟨ ( ( 1^st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1^st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2^nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2^nd ‘ ( 𝑡 · 𝑓 ) ) ) ⟩ )
180	172 174 179	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) )
181	2 3 4	tendocoval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ∧ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ) → ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( 𝑠 ‘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) )
182	121 122 123 125 181	syl121anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) = ( 𝑠 ‘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) )
183		coass	⊢ ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) )
184	183	a1i	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) )
185	182 184	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( 𝑠 ‘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) ⟩ )
186	2 4	tendococl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 )
187	121 122 123 186	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 )
188	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
189	121 187 124 188	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
190	2 3 4	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ) → ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ∈ 𝑇 )
191	121 123 125 190	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ∈ 𝑇 )
192	2 4	tendococl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ ( 2^nd ‘ 𝑓 ) ∈ 𝐸 ) → ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 )
193	121 123 151 192	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 )
194	2 3 4 5 12	dvhopvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ∈ 𝑇 ∧ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 ) ) → ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ⟨ ( 𝑠 ‘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) ⟩ )
195	121 122 191 193 194	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ⟨ ( 𝑠 ‘ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ) ⟩ )
196	185 189 195	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
197	2 3 4 5 6 11	dvhmulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
198	197	3adantr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
199	198	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) )
200	138	oveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 · 𝑓 ) ) = ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1^st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
201	196 199 200	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( 𝑠 · ( 𝑡 · 𝑓 ) ) )
202		xp1st	⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → ( 1^st ‘ 𝑠 ) ∈ 𝑇 )
203	202	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( 1^st ‘ 𝑠 ) ∈ 𝑇 )
204		fvresi	⊢ ( ( 1^st ‘ 𝑠 ) ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ 𝑠 ) )
205	203 204	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ 𝑠 ) )
206		xp2nd	⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝑠 ) ∈ 𝐸 )
207	2 3 4	tendof	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2^nd ‘ 𝑠 ) ∈ 𝐸 ) → ( 2^nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 )
208	206 207	sylan2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( 2^nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 )
209		fcoi2	⊢ ( ( 2^nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 → ( ( I ↾ 𝑇 ) ∘ ( 2^nd ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) )
210	208 209	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ∘ ( 2^nd ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) )
211	205 210	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ⟨ ( ( I ↾ 𝑇 ) ‘ ( 1^st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2^nd ‘ 𝑠 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑠 ) , ( 2^nd ‘ 𝑠 ) ⟩ )
212	2 3 4	tendoidcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
213	212	anim1i	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) )
214	2 3 4 5 12	dvhvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = ⟨ ( ( I ↾ 𝑇 ) ‘ ( 1^st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2^nd ‘ 𝑠 ) ) ⟩ )
215	213 214	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = ⟨ ( ( I ↾ 𝑇 ) ‘ ( 1^st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2^nd ‘ 𝑠 ) ) ⟩ )
216		1st2nd2	⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → 𝑠 = ⟨ ( 1^st ‘ 𝑠 ) , ( 2^nd ‘ 𝑠 ) ⟩ )
217	216	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → 𝑠 = ⟨ ( 1^st ‘ 𝑠 ) , ( 2^nd ‘ 𝑠 ) ⟩ )
218	211 215 217	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = 𝑠 )
219	15 16 17 18 21 22 23 29 33 34 36 120 180 201 218	islmodd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LMod )
220	6	islvec	⊢ ( 𝑈 ∈ LVec ↔ ( 𝑈 ∈ LMod ∧ 𝐷 ∈ DivRing ) )
221	219 31 220	sylanbrc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )

Metamath Proof Explorer

Theorem dvhlveclem

Proof