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 ) |