Metamath Proof Explorer


Theorem dvalveclem

Description: Lemma for dvalvec . (Contributed by NM, 11-Oct-2013) (Proof shortened by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvalvec.h 𝐻 = ( LHyp ‘ 𝐾 )
dvalvec.v 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dvalveclem.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvalveclem.a + = ( +g𝑈 )
dvalveclem.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvalveclem.d 𝐷 = ( Scalar ‘ 𝑈 )
dvalveclem.b 𝐵 = ( Base ‘ 𝐾 )
dvalveclem.p = ( +g𝐷 )
dvalveclem.m × = ( .r𝐷 )
dvalveclem.s · = ( ·𝑠𝑈 )
Assertion dvalveclem ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ LVec )

Proof

Step Hyp Ref Expression
1 dvalvec.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dvalvec.v 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
3 dvalveclem.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dvalveclem.a + = ( +g𝑈 )
5 dvalveclem.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 dvalveclem.d 𝐷 = ( Scalar ‘ 𝑈 )
7 dvalveclem.b 𝐵 = ( Base ‘ 𝐾 )
8 dvalveclem.p = ( +g𝐷 )
9 dvalveclem.m × = ( .r𝐷 )
10 dvalveclem.s · = ( ·𝑠𝑈 )
11 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
12 1 3 2 11 dvavbase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ 𝑈 ) = 𝑇 )
13 12 eqcomd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑇 = ( Base ‘ 𝑈 ) )
14 4 a1i ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → + = ( +g𝑈 ) )
15 6 a1i ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 = ( Scalar ‘ 𝑈 ) )
16 10 a1i ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → · = ( ·𝑠𝑈 ) )
17 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 1 5 2 6 17 dvabase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
19 18 eqcomd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) )
20 8 a1i ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → = ( +g𝐷 ) )
21 9 a1i ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → × = ( .r𝐷 ) )
22 1 3 5 tendoidcl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
23 22 19 eleqtrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) )
24 eqid ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) ) = ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) )
25 7 1 3 5 24 tendo1ne0 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝑇 ) ≠ ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) ) )
26 eqid ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
27 1 26 2 6 dvasca ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
28 27 fveq2d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 0g𝐷 ) = ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) )
29 eqid ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
30 7 1 3 26 24 29 erng0g ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 0g ‘ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) ) )
31 28 30 eqtrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 0g𝐷 ) = ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) ) )
32 25 31 neeqtrrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝑇 ) ≠ ( 0g𝐷 ) )
33 22 22 jca ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) )
34 1 3 5 2 6 9 dvamulr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) → ( ( I ↾ 𝑇 ) × ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) )
35 33 34 mpdan ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( I ↾ 𝑇 ) × ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) )
36 f1oi ( I ↾ 𝑇 ) : 𝑇1-1-onto𝑇
37 f1of ( ( I ↾ 𝑇 ) : 𝑇1-1-onto𝑇 → ( I ↾ 𝑇 ) : 𝑇𝑇 )
38 fcoi2 ( ( I ↾ 𝑇 ) : 𝑇𝑇 → ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) )
39 36 37 38 mp2b ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 )
40 35 39 eqtrdi ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( I ↾ 𝑇 ) × ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) )
41 23 32 40 3jca ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ( I ↾ 𝑇 ) ≠ ( 0g𝐷 ) ∧ ( ( I ↾ 𝑇 ) × ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) ) )
42 1 26 erngdv ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
43 27 42 eqeltrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 ∈ DivRing )
44 eqid ( 0g𝐷 ) = ( 0g𝐷 )
45 eqid ( 1r𝐷 ) = ( 1r𝐷 )
46 17 9 44 45 drngid2 ( 𝐷 ∈ DivRing → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ( I ↾ 𝑇 ) ≠ ( 0g𝐷 ) ∧ ( ( I ↾ 𝑇 ) × ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) ) ↔ ( 1r𝐷 ) = ( I ↾ 𝑇 ) ) )
47 43 46 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ( I ↾ 𝑇 ) ≠ ( 0g𝐷 ) ∧ ( ( I ↾ 𝑇 ) × ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) ) ↔ ( 1r𝐷 ) = ( I ↾ 𝑇 ) ) )
48 41 47 mpbid ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 1r𝐷 ) = ( I ↾ 𝑇 ) )
49 48 eqcomd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝑇 ) = ( 1r𝐷 ) )
50 drngring ( 𝐷 ∈ DivRing → 𝐷 ∈ Ring )
51 43 50 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐷 ∈ Ring )
52 1 2 dvaabl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ Abel )
53 ablgrp ( 𝑈 ∈ Abel → 𝑈 ∈ Grp )
54 52 53 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ Grp )
55 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇 ) ) → ( 𝑠 · 𝑡 ) = ( 𝑠𝑡 ) )
56 55 3impb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝑇 ) → ( 𝑠 · 𝑡 ) = ( 𝑠𝑡 ) )
57 1 3 5 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝑇 ) → ( 𝑠𝑡 ) ∈ 𝑇 )
58 56 57 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝑇 ) → ( 𝑠 · 𝑡 ) ∈ 𝑇 )
59 1 3 5 tendospdi1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 ‘ ( 𝑡𝑓 ) ) = ( ( 𝑠𝑡 ) ∘ ( 𝑠𝑓 ) ) )
60 simpr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → 𝑠𝐸 )
61 1 3 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑡𝑇𝑓𝑇 ) → ( 𝑡𝑓 ) ∈ 𝑇 )
62 61 3adant3r1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑡𝑓 ) ∈ 𝑇 )
63 60 62 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠𝐸 ∧ ( 𝑡𝑓 ) ∈ 𝑇 ) )
64 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸 ∧ ( 𝑡𝑓 ) ∈ 𝑇 ) ) → ( 𝑠 · ( 𝑡𝑓 ) ) = ( 𝑠 ‘ ( 𝑡𝑓 ) ) )
65 63 64 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 · ( 𝑡𝑓 ) ) = ( 𝑠 ‘ ( 𝑡𝑓 ) ) )
66 57 3adant3r3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠𝑡 ) ∈ 𝑇 )
67 1 3 5 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑓𝑇 ) → ( 𝑠𝑓 ) ∈ 𝑇 )
68 67 3adant3r2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠𝑓 ) ∈ 𝑇 )
69 66 68 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) ∈ 𝑇 ∧ ( 𝑠𝑓 ) ∈ 𝑇 ) )
70 1 3 2 4 dvavadd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑠𝑡 ) ∈ 𝑇 ∧ ( 𝑠𝑓 ) ∈ 𝑇 ) ) → ( ( 𝑠𝑡 ) + ( 𝑠𝑓 ) ) = ( ( 𝑠𝑡 ) ∘ ( 𝑠𝑓 ) ) )
71 69 70 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) + ( 𝑠𝑓 ) ) = ( ( 𝑠𝑡 ) ∘ ( 𝑠𝑓 ) ) )
72 59 65 71 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 · ( 𝑡𝑓 ) ) = ( ( 𝑠𝑡 ) + ( 𝑠𝑓 ) ) )
73 1 3 2 4 dvavadd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑡𝑇𝑓𝑇 ) ) → ( 𝑡 + 𝑓 ) = ( 𝑡𝑓 ) )
74 73 3adantr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑡 + 𝑓 ) = ( 𝑡𝑓 ) )
75 74 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ( 𝑠 · ( 𝑡𝑓 ) ) )
76 55 3adantr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 · 𝑡 ) = ( 𝑠𝑡 ) )
77 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑓𝑇 ) ) → ( 𝑠 · 𝑓 ) = ( 𝑠𝑓 ) )
78 77 3adantr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 · 𝑓 ) = ( 𝑠𝑓 ) )
79 76 78 oveq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) = ( ( 𝑠𝑡 ) + ( 𝑠𝑓 ) ) )
80 72 75 79 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝑇𝑓𝑇 ) ) → ( 𝑠 · ( 𝑡 + 𝑓 ) ) = ( ( 𝑠 · 𝑡 ) + ( 𝑠 · 𝑓 ) ) )
81 1 3 5 2 6 8 dvaplusgv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 𝑡 ) ‘ 𝑓 ) = ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) )
82 1 3 5 2 6 8 dvafplusg ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → = ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) ) )
83 82 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → = ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) ) )
84 83 oveqd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 𝑡 ) = ( 𝑠 ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) ) 𝑡 ) )
85 eqid ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) ) = ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) )
86 1 3 5 85 tendoplcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 ( 𝑎𝐸 , 𝑏𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑎𝑓 ) ∘ ( 𝑏𝑓 ) ) ) ) 𝑡 ) ∈ 𝐸 )
87 84 86 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠 𝑡 ) ∈ 𝐸 )
88 87 3adant3r3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠 𝑡 ) ∈ 𝐸 )
89 simpr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → 𝑓𝑇 )
90 88 89 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 𝑡 ) ∈ 𝐸𝑓𝑇 ) )
91 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑠 𝑡 ) ∈ 𝐸𝑓𝑇 ) ) → ( ( 𝑠 𝑡 ) · 𝑓 ) = ( ( 𝑠 𝑡 ) ‘ 𝑓 ) )
92 90 91 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 𝑡 ) · 𝑓 ) = ( ( 𝑠 𝑡 ) ‘ 𝑓 ) )
93 77 3adantr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠 · 𝑓 ) = ( 𝑠𝑓 ) )
94 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑡𝐸𝑓𝑇 ) ) → ( 𝑡 · 𝑓 ) = ( 𝑡𝑓 ) )
95 94 3adantr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑡 · 𝑓 ) = ( 𝑡𝑓 ) )
96 93 95 oveq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = ( ( 𝑠𝑓 ) + ( 𝑡𝑓 ) ) )
97 67 3adant3r2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠𝑓 ) ∈ 𝑇 )
98 1 3 5 tendospcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑡𝐸𝑓𝑇 ) → ( 𝑡𝑓 ) ∈ 𝑇 )
99 98 3adant3r1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑡𝑓 ) ∈ 𝑇 )
100 97 99 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑓 ) ∈ 𝑇 ∧ ( 𝑡𝑓 ) ∈ 𝑇 ) )
101 1 3 2 4 dvavadd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑠𝑓 ) ∈ 𝑇 ∧ ( 𝑡𝑓 ) ∈ 𝑇 ) ) → ( ( 𝑠𝑓 ) + ( 𝑡𝑓 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) )
102 100 101 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑓 ) + ( 𝑡𝑓 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) )
103 96 102 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) )
104 81 92 103 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 𝑡 ) · 𝑓 ) = ( ( 𝑠 · 𝑓 ) + ( 𝑡 · 𝑓 ) ) )
105 1 3 5 tendospass ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) ‘ 𝑓 ) = ( 𝑠 ‘ ( 𝑡𝑓 ) ) )
106 1 5 tendococl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝐸𝑡𝐸 ) → ( 𝑠𝑡 ) ∈ 𝐸 )
107 106 3adant3r3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠𝑡 ) ∈ 𝐸 )
108 107 89 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) ∈ 𝐸𝑓𝑇 ) )
109 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑠𝑡 ) ∈ 𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) · 𝑓 ) = ( ( 𝑠𝑡 ) ‘ 𝑓 ) )
110 108 109 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) · 𝑓 ) = ( ( 𝑠𝑡 ) ‘ 𝑓 ) )
111 simpr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → 𝑠𝐸 )
112 111 99 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠𝐸 ∧ ( 𝑡𝑓 ) ∈ 𝑇 ) )
113 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸 ∧ ( 𝑡𝑓 ) ∈ 𝑇 ) ) → ( 𝑠 · ( 𝑡𝑓 ) ) = ( 𝑠 ‘ ( 𝑡𝑓 ) ) )
114 112 113 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠 · ( 𝑡𝑓 ) ) = ( 𝑠 ‘ ( 𝑡𝑓 ) ) )
115 105 110 114 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠𝑡 ) · 𝑓 ) = ( 𝑠 · ( 𝑡𝑓 ) ) )
116 1 3 5 2 6 9 dvamulr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸 ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠𝑡 ) )
117 116 3adantr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠 × 𝑡 ) = ( 𝑠𝑡 ) )
118 117 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( ( 𝑠𝑡 ) · 𝑓 ) )
119 95 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( 𝑠 · ( 𝑡 · 𝑓 ) ) = ( 𝑠 · ( 𝑡𝑓 ) ) )
120 115 118 119 3eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑠𝐸𝑡𝐸𝑓𝑇 ) ) → ( ( 𝑠 × 𝑡 ) · 𝑓 ) = ( 𝑠 · ( 𝑡 · 𝑓 ) ) )
121 22 anim1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝑇 ) → ( ( I ↾ 𝑇 ) ∈ 𝐸𝑠𝑇 ) )
122 1 3 5 2 10 dvavsca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸𝑠𝑇 ) ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = ( ( I ↾ 𝑇 ) ‘ 𝑠 ) )
123 121 122 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝑇 ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = ( ( I ↾ 𝑇 ) ‘ 𝑠 ) )
124 fvresi ( 𝑠𝑇 → ( ( I ↾ 𝑇 ) ‘ 𝑠 ) = 𝑠 )
125 124 adantl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝑇 ) → ( ( I ↾ 𝑇 ) ‘ 𝑠 ) = 𝑠 )
126 123 125 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑠𝑇 ) → ( ( I ↾ 𝑇 ) · 𝑠 ) = 𝑠 )
127 13 14 15 16 19 20 21 49 51 54 58 80 104 120 126 islmodd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ LMod )
128 6 islvec ( 𝑈 ∈ LVec ↔ ( 𝑈 ∈ LMod ∧ 𝐷 ∈ DivRing ) )
129 127 43 128 sylanbrc ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑈 ∈ LVec )