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 )