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 )