Metamath Proof Explorer

Theorem 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 = ( 0g ‘ 𝐷 )
dvhgrp.i ⊢ 𝐼 = ( invg ‘ 𝐷 )
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 = ( 0g ‘ 𝐷 )
10 dvhgrp.i ⊢ 𝐼 = ( invg ‘ 𝐷 )
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 ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐷 ) = ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
27 eqid ⊢ ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
28 2 3 24 27 erng1r ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( I ↾ 𝑇 ) )
29 26 28 eqtr2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) = ( 1r ‘ 𝐷 ) )
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 ⊢ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝑡 ) ∈ 𝑇 )
41 39 40 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝑡 ) ∈ 𝑇 )
42 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑓 ∈ ( 𝑇 × 𝐸 ) )
43 xp1st ⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝑓 ) ∈ 𝑇 )
44 42 43 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝑓 ) ∈ 𝑇 )
45 2 3 4 tendospdi1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 1st ‘ 𝑡 ) ∈ 𝑇 ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) ) → ( 𝑠 ‘ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) )
46 37 38 41 44 45 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) )
47 2 3 4 5 6 8 7 dvhvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) = ⟨ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ⟩ )
48 47 3adantr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) = ⟨ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ⟩ )
49 48 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 + 𝑓 ) ) = ( 1st ‘ ⟨ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
50 fvex ⊢ ( 1st ‘ 𝑡 ) ∈ V
51 fvex ⊢ ( 1st ‘ 𝑓 ) ∈ V
52 50 51 coex ⊢ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ∈ V
53 ovex ⊢ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ V
54 52 53 op1st ⊢ ( 1st ‘ ⟨ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) )
55 49 54 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 + 𝑓 ) ) = ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) )
56 55 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) = ( 𝑠 ‘ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) ) )
57 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) = ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ )
58 57 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑡 ) = ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ )
59 58 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑡 ) ) = ( 1st ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) )
60 fvex ⊢ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∈ V
61 vex ⊢ 𝑠 ∈ V
62 fvex ⊢ ( 2nd ‘ 𝑡 ) ∈ V
63 61 62 coex ⊢ ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ∈ V
64 60 63 op1st ⊢ ( 1st ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) = ( 𝑠 ‘ ( 1st ‘ 𝑡 ) )
65 59 64 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑡 ) ) = ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) )
66 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
67 66 3adantr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
68 67 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 1st ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
69 fvex ⊢ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∈ V
70 fvex ⊢ ( 2nd ‘ 𝑓 ) ∈ V
71 61 70 coex ⊢ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ∈ V
72 69 71 op1st ⊢ ( 1st ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑠 ‘ ( 1st ‘ 𝑓 ) )
73 68 72 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) )
74 65 73 coeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) ∘ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ) )
75 46 56 74 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) = ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) )
76 33 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐷 ∈ Ring )
77 21 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) )
78 38 77 eleqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐷 ) )
79 xp2nd ⊢ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑡 ) ∈ 𝐸 )
80 39 79 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑡 ) ∈ 𝐸 )
81 80 77 eleqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) )
82 xp2nd ⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 )
83 42 82 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 )
84 83 77 eleqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) )
85 19 7 11 ringdi ⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ) )
86 76 78 81 84 85 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ) )
87 19 7 ringacl ⊢ ( ( 𝐷 ∈ Ring ∧ ( 2nd ‘ 𝑡 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) )
88 76 81 84 87 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) )
89 88 77 eleqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 )
90 2 3 4 5 6 11 dvhmulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) )
91 37 38 89 90 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) )
92 2 3 4 5 6 11 dvhmulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 2nd ‘ 𝑡 ) ∈ 𝐸 ) ) → ( 𝑠 × ( 2nd ‘ 𝑡 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) )
93 37 38 80 92 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2nd ‘ 𝑡 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) )
94 2 3 4 5 6 11 dvhmulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( 𝑠 × ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) )
95 37 38 83 94 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) )
96 93 95 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) )
97 86 91 96 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) )
98 48 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 + 𝑓 ) ) = ( 2nd ‘ ⟨ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
99 52 53 op2nd ⊢ ( 2nd ‘ ⟨ ( ( 1st ‘ 𝑡 ) ∘ ( 1st ‘ 𝑓 ) ) , ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) )
100 98 99 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 + 𝑓 ) ) = ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) )
101 100 coeq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) = ( 𝑠 ∘ ( ( 2nd ‘ 𝑡 ) ⨣ ( 2nd ‘ 𝑓 ) ) ) )
102 58 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑡 ) ) = ( 2nd ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) )
103 60 63 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑡 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) )
104 102 103 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑡 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) )
105 67 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 2nd ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
106 69 71 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) )
107 105 106 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) )
108 104 107 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑡 ) ) ⨣ ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ) )
109 97 101 108 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) = ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) )
110 75 109 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) ⟩ )
111 2 3 4 5 6 7 8 dvhvaddcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
112 111 3adantr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) )
113 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 + 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ⟨ ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) ⟩ )
114 37 38 112 113 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ⟨ ( 𝑠 ‘ ( 1st ‘ ( 𝑡 + 𝑓 ) ) ) , ( 𝑠 ∘ ( 2nd ‘ ( 𝑡 + 𝑓 ) ) ) ⟩ )
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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 · 𝑡 ) ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = ⟨ ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) ⟩ )
119 37 115 117 118 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = ⟨ ( ( 1st ‘ ( 𝑠 · 𝑡 ) ) ∘ ( 1st ‘ ( 𝑠 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑡 ) ) ⨣ ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ) ⟩ )
120 110 114 119 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) )
121 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
122 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑠 ∈ 𝐸 )
123 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑡 ∈ 𝐸 )
124 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑓 ∈ ( 𝑇 × 𝐸 ) )
125 124 43 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝑓 ) ∈ 𝑇 )
126 eqid ⊢ ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
127 2 3 4 24 126 erngplus2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) ) → ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) )
128 121 122 123 125 127 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) )
129 25 fveq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝐷 ) = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
130 7 129 syl5eq ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
131 130 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 ⨣ 𝑡 ) = ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) )
132 131 fveq1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) )
133 132 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 𝑠 ( +g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) )
134 66 3adantr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · 𝑓 ) = ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
135 134 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 1st ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
136 135 72 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) )
137 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) = ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
138 137 3adantr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 · 𝑓 ) = ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
139 138 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 · 𝑓 ) ) = ( 1st ‘ ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
140 fvex ⊢ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ V
141 vex ⊢ 𝑡 ∈ V
142 141 70 coex ⊢ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ V
143 140 142 op1st ⊢ ( 1st ‘ ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑡 ‘ ( 1st ‘ 𝑓 ) )
144 139 143 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ ( 𝑡 · 𝑓 ) ) = ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) )
145 136 144 coeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) = ( ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) ∘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) )
146 128 133 145 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) )
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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ 𝐸 )
152 151 148 eleqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) )
153 19 7 11 ringdir ⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝑠 ∈ ( Base ‘ 𝐷 ) ∧ 𝑡 ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2nd ‘ 𝑓 ) ) ) )
154 147 149 150 152 153 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2nd ‘ 𝑓 ) ) ) )
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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) )
159 121 157 151 158 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) × ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) )
160 121 122 151 94 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) )
161 2 3 4 5 6 11 dvhmulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( 𝑡 × ( 2nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) )
162 121 123 151 161 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 × ( 2nd ‘ 𝑓 ) ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) )
163 160 162 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 × ( 2nd ‘ 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) )
164 154 159 163 3eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) )
165 134 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 2nd ‘ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
166 165 106 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑠 · 𝑓 ) ) = ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) )
167 138 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 · 𝑓 ) ) = ( 2nd ‘ ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
168 140 142 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) )
169 167 168 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ ( 𝑡 · 𝑓 ) ) = ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) )
170 166 169 oveq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) = ( ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⨣ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) )
171 164 170 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) )
172 146 171 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) ⟩ )
173 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ⨣ 𝑡 ) ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
174 121 157 124 173 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ⨣ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ⨣ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ∧ ( 𝑡 · 𝑓 ) ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = ⟨ ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) ⟩ )
179 121 175 177 178 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = ⟨ ( ( 1st ‘ ( 𝑠 · 𝑓 ) ) ∘ ( 1st ‘ ( 𝑡 · 𝑓 ) ) ) , ( ( 2nd ‘ ( 𝑠 · 𝑓 ) ) ⨣ ( 2nd ‘ ( 𝑡 · 𝑓 ) ) ) ⟩ )
180 172 174 179 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ⨣ 𝑡 ) · 𝑓 ) = ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) )
181 2 3 4 tendocoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) → ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) )
182 121 122 123 125 181 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) = ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) )
183 coass ⊢ ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) )
184 183 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) = ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) )
185 182 184 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ⟩ = ⟨ ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ⟩ )
186 2 4 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) → ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 )
187 121 122 123 186 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 )
188 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑠 ∘ 𝑡 ) ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
189 121 187 124 188 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ⟨ ( ( 𝑠 ∘ 𝑡 ) ‘ ( 1st ‘ 𝑓 ) ) , ( ( 𝑠 ∘ 𝑡 ) ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
190 2 3 4 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ ( 1st ‘ 𝑓 ) ∈ 𝑇 ) → ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ 𝑇 )
191 121 123 125 190 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ 𝑇 )
192 2 4 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ ( 2nd ‘ 𝑓 ) ∈ 𝐸 ) → ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 )
193 121 123 151 192 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 )
194 2 3 4 5 12 dvhopvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ∈ 𝑇 ∧ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ∈ 𝐸 ) ) → ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ⟨ ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ⟩ )
195 121 122 191 193 194 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) = ⟨ ( 𝑠 ‘ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) ) , ( 𝑠 ∘ ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ) ⟩ )
196 185 189 195 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) = ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
197 2 3 4 5 6 11 dvhmulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
198 197 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠 ∘ 𝑡 ) )
199 198 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( ( 𝑠 ∘ 𝑡 ) · 𝑓 ) )
200 138 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑠 · ( 𝑡 · 𝑓 ) ) = ( 𝑠 · ⟨ ( 𝑡 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ ) )
201 196 199 200 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( 𝑠 · ( 𝑡 · 𝑓 ) ) )
202 xp1st ⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝑠 ) ∈ 𝑇 )
203 202 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( 1st ‘ 𝑠 ) ∈ 𝑇 )
204 fvresi ⊢ ( ( 1st ‘ 𝑠 ) ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) = ( 1st ‘ 𝑠 ) )
205 203 204 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) = ( 1st ‘ 𝑠 ) )
206 xp2nd ⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝑠 ) ∈ 𝐸 )
207 2 3 4 tendof ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2nd ‘ 𝑠 ) ∈ 𝐸 ) → ( 2nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 )
208 206 207 sylan2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( 2nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 )
209 fcoi2 ⊢ ( ( 2nd ‘ 𝑠 ) : 𝑇 ⟶ 𝑇 → ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) )
210 208 209 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) )
211 205 210 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ⟨ ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) ⟩ = ⟨ ( 1st ‘ 𝑠 ) , ( 2nd ‘ 𝑠 ) ⟩ )
212 2 3 4 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
213 212 anim1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) )
214 2 3 4 5 12 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = ⟨ ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) ⟩ )
215 213 214 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = ⟨ ( ( I ↾ 𝑇 ) ‘ ( 1st ‘ 𝑠 ) ) , ( ( I ↾ 𝑇 ) ∘ ( 2nd ‘ 𝑠 ) ) ⟩ )
216 1st2nd2 ⊢ ( 𝑠 ∈ ( 𝑇 × 𝐸 ) → 𝑠 = ⟨ ( 1st ‘ 𝑠 ) , ( 2nd ‘ 𝑠 ) ⟩ )
217 216 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( 𝑇 × 𝐸 ) ) → 𝑠 = ⟨ ( 1st ‘ 𝑠 ) , ( 2nd ‘ 𝑠 ) ⟩ )
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 )