Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (Scalar‘𝑈) = (Scalar‘𝑈)) |
2 | | diblss.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | eqid 2622 |
. . . . 5
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) |
4 | | diblss.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | eqid 2622 |
. . . . 5
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
6 | | eqid 2622 |
. . . . 5
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
7 | 2, 3, 4, 5, 6 | dvhbase 36372 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊)) |
8 | 7 | eqcomd 2628 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((TEndo‘𝐾)‘𝑊) = (Base‘(Scalar‘𝑈))) |
9 | 8 | adantr 481 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((TEndo‘𝐾)‘𝑊) = (Base‘(Scalar‘𝑈))) |
10 | | eqid 2622 |
. . . . 5
⊢
((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) |
11 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
12 | 2, 10, 3, 4, 11 | dvhvbase 36376 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
13 | 12 | eqcomd 2628 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) = (Base‘𝑈)) |
14 | 13 | adantr 481 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) = (Base‘𝑈)) |
15 | | eqidd 2623 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (+g‘𝑈) = (+g‘𝑈)) |
16 | | eqidd 2623 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈)) |
17 | | diblss.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑈) |
18 | 17 | a1i 11 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → 𝑆 = (LSubSp‘𝑈)) |
19 | | diblss.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
20 | | diblss.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
21 | | diblss.i |
. . . 4
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
22 | 19, 20, 2, 21, 4, 11 | dibss 36458 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ (Base‘𝑈)) |
23 | 22, 14 | sseqtr4d 3642 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
24 | 19, 20, 2, 21 | dibn0 36442 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅) |
25 | | fvex 6201 |
. . . . . . 7
⊢ (𝑥‘(1st
‘𝑎)) ∈
V |
26 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
27 | | fvex 6201 |
. . . . . . . 8
⊢
(2nd ‘𝑎) ∈ V |
28 | 26, 27 | coex 7118 |
. . . . . . 7
⊢ (𝑥 ∘ (2nd
‘𝑎)) ∈
V |
29 | 25, 28 | op1st 7176 |
. . . . . 6
⊢
(1st ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) = (𝑥‘(1st ‘𝑎)) |
30 | 29 | coeq1i 5281 |
. . . . 5
⊢
((1st ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏))
= ((𝑥‘(1st
‘𝑎)) ∘
(1st ‘𝑏)) |
31 | | simpll 790 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
32 | | simpr1 1067 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) |
33 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
34 | | simpr2 1068 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑎 ∈ (𝐼‘𝑋)) |
35 | 19, 20, 2, 10, 21 | dibelval1st1 36439 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋)) → (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) |
36 | 31, 33, 34, 35 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) |
37 | 2, 10, 3 | tendocl 36055 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊)) |
38 | 31, 32, 36, 37 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊)) |
39 | | simpr3 1069 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑏 ∈ (𝐼‘𝑋)) |
40 | 19, 20, 2, 10, 21 | dibelval1st1 36439 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑏 ∈ (𝐼‘𝑋)) → (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) |
41 | 31, 33, 39, 40 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) |
42 | 2, 10 | ltrnco 36007 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → ((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
((LTrn‘𝐾)‘𝑊)) |
43 | 31, 38, 41, 42 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
((LTrn‘𝐾)‘𝑊)) |
44 | | simplll 798 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝐾 ∈ HL) |
45 | | hllat 34650 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝐾 ∈ Lat) |
47 | | eqid 2622 |
. . . . . . . . 9
⊢
((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊) |
48 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ∈ 𝐵) |
49 | 31, 43, 48 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ∈ 𝐵) |
50 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵) |
51 | 31, 38, 50 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵) |
52 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵) |
53 | 31, 41, 52 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵) |
54 | | eqid 2622 |
. . . . . . . . 9
⊢
(join‘𝐾) =
(join‘𝐾) |
55 | 19, 54 | latjcl 17051 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧
(((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ∈ 𝐵) |
56 | 46, 51, 53, 55 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ∈ 𝐵) |
57 | | simplrl 800 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑋 ∈ 𝐵) |
58 | 20, 54, 2, 10, 47 | trlco 36015 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥‘(1st ‘𝑎)) ∈ ((LTrn‘𝐾)‘𝑊) ∧ (1st ‘𝑏) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ≤
((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)))) |
59 | 31, 38, 41, 58 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ≤
((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)))) |
60 | 19, 2, 10, 47 | trlcl 35451 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ∈ 𝐵) |
61 | 31, 36, 60 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ∈ 𝐵) |
62 | 20, 2, 10, 47, 3 | tendotp 36049 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (1st ‘𝑎) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎))) |
63 | 31, 32, 36, 62 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎))) |
64 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊) |
65 | 19, 20, 2, 64, 21 | dibelval1st 36438 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋)) → (1st ‘𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) |
66 | 31, 33, 34, 65 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) |
67 | 19, 20, 2, 10, 47, 64 | diatrl 36333 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (1st ‘𝑎) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ≤ 𝑋) |
68 | 31, 33, 66, 67 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑎)) ≤ 𝑋) |
69 | 19, 20, 46, 51, 61, 57, 63, 68 | lattrd 17058 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ 𝑋) |
70 | 19, 20, 2, 64, 21 | dibelval1st 36438 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑏 ∈ (𝐼‘𝑋)) → (1st ‘𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) |
71 | 31, 33, 39, 70 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (1st ‘𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) |
72 | 19, 20, 2, 10, 47, 64 | diatrl 36333 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (1st ‘𝑏) ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋) |
73 | 31, 33, 71, 72 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋) |
74 | 19, 20, 54 | latjle12 17062 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧
((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ∈ 𝐵 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ 𝑋 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋) ↔ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ≤ 𝑋)) |
75 | 46, 51, 53, 57, 74 | syl13anc 1328 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎))) ≤ 𝑋 ∧ (((trL‘𝐾)‘𝑊)‘(1st ‘𝑏)) ≤ 𝑋) ↔ ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ≤ 𝑋)) |
76 | 69, 73, 75 | mpbi2and 956 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((((trL‘𝐾)‘𝑊)‘(𝑥‘(1st ‘𝑎)))(join‘𝐾)(((trL‘𝐾)‘𝑊)‘(1st ‘𝑏))) ≤ 𝑋) |
77 | 19, 20, 46, 49, 56, 57, 59, 76 | lattrd 17058 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ≤ 𝑋) |
78 | 19, 20, 2, 10, 47, 64 | diaelval 36322 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
(((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
((LTrn‘𝐾)‘𝑊) ∧ (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ≤ 𝑋))) |
79 | 78 | adantr 481 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
(((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
((LTrn‘𝐾)‘𝑊) ∧ (((trL‘𝐾)‘𝑊)‘((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏))) ≤ 𝑋))) |
80 | 43, 77, 79 | mpbir2and 957 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥‘(1st ‘𝑎)) ∘ (1st
‘𝑏)) ∈
(((DIsoA‘𝐾)‘𝑊)‘𝑋)) |
81 | 30, 80 | syl5eqel 2705 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((1st
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏))
∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋)) |
82 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ)))) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ)))) |
83 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘(Scalar‘𝑈)) =
(+g‘(Scalar‘𝑈)) |
84 | 2, 10, 3, 4, 5, 82,
83 | dvhfplusr 36373 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))) |
85 | 84 | ad2antrr 762 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) →
(+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))) |
86 | 25, 28 | op2nd 7177 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) = (𝑥 ∘ (2nd ‘𝑎)) |
87 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) |
88 | 19, 20, 2, 10, 87, 21 | dibelval2nd 36441 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋)) → (2nd ‘𝑎) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
89 | 31, 33, 34, 88 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘𝑎) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
90 | 89 | coeq2d 5284 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (2nd ‘𝑎)) = (𝑥 ∘ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))) |
91 | 19, 2, 10, 3, 87 | tendo0mulr 36115 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
92 | 31, 32, 91 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
93 | 90, 92 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (2nd ‘𝑎)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
94 | 86, 93 | syl5eq 2668 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
95 | 19, 20, 2, 10, 87, 21 | dibelval2nd 36441 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑏 ∈ (𝐼‘𝑋)) → (2nd ‘𝑏) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
96 | 31, 33, 39, 95 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘𝑏) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
97 | 85, 94, 96 | oveq123d 6671 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((2nd
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) = ((ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)))) |
98 | | simpllr 799 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑊 ∈ 𝐻) |
99 | 19, 2, 10, 3, 87 | tendo0cl 36078 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) |
100 | 99 | ad2antrr 762 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) |
101 | 19, 2, 10, 3, 87, 82 | tendo0pl 36079 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) → ((ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
102 | 44, 98, 100, 101 | syl21anc 1325 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ((𝑠‘ℎ) ∘ (𝑡‘ℎ))))(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
103 | 97, 102 | eqtrd 2656 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((2nd
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
104 | | ovex 6678 |
. . . . . 6
⊢
((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ V |
105 | 104 | elsn 4192 |
. . . . 5
⊢
(((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))} ↔ ((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))) |
106 | 103, 105 | sylibr 224 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((2nd
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) |
107 | | opelxpi 5148 |
. . . 4
⊢
((((1st ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏))
∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ ((2nd ‘〈(𝑥‘(1st
‘𝑎)), (𝑥 ∘ (2nd
‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏)) ∈ {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))}) → 〈((1st
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘ (1st
‘𝑏)), ((2nd
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))〉 ∈
((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})) |
108 | 81, 106, 107 | syl2anc 693 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 〈((1st
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏)),
((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))〉 ∈
((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})) |
109 | 23 | adantr 481 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝐼‘𝑋) ⊆ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
110 | 109, 34 | sseldd 3604 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑎 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
111 | | eqid 2622 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
112 | 2, 10, 3, 4, 111 | dvhvsca 36390 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))) → (𝑥( ·𝑠
‘𝑈)𝑎) = 〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) |
113 | 31, 32, 110, 112 | syl12anc 1324 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥( ·𝑠
‘𝑈)𝑎) = 〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) |
114 | 113 | oveq1d 6665 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) = (〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉(+g‘𝑈)𝑏)) |
115 | 89, 100 | eqeltrd 2701 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (2nd ‘𝑎) ∈ ((TEndo‘𝐾)‘𝑊)) |
116 | 2, 3 | tendococl 36060 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (2nd ‘𝑎) ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑥 ∘ (2nd ‘𝑎)) ∈ ((TEndo‘𝐾)‘𝑊)) |
117 | 31, 32, 115, 116 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝑥 ∘ (2nd ‘𝑎)) ∈ ((TEndo‘𝐾)‘𝑊)) |
118 | | opelxpi 5148 |
. . . . . 6
⊢ (((𝑥‘(1st
‘𝑎)) ∈
((LTrn‘𝐾)‘𝑊) ∧ (𝑥 ∘ (2nd ‘𝑎)) ∈ ((TEndo‘𝐾)‘𝑊)) → 〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉 ∈
(((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
119 | 38, 117, 118 | syl2anc 693 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉 ∈
(((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
120 | 109, 39 | sseldd 3604 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → 𝑏 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))) |
121 | | eqid 2622 |
. . . . . 6
⊢
(+g‘𝑈) = (+g‘𝑈) |
122 | 2, 10, 3, 4, 5, 121, 83 | dvhvadd 36381 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉 ∈
(((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) ∧ 𝑏 ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))) → (〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉(+g‘𝑈)𝑏) = 〈((1st
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏)),
((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))〉) |
123 | 31, 119, 120, 122 | syl12anc 1324 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉(+g‘𝑈)𝑏) = 〈((1st
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏)),
((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))〉) |
124 | 114, 123 | eqtrd 2656 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) = 〈((1st
‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉) ∘
(1st ‘𝑏)),
((2nd ‘〈(𝑥‘(1st ‘𝑎)), (𝑥 ∘ (2nd ‘𝑎))〉)(+g‘(Scalar‘𝑈))(2nd ‘𝑏))〉) |
125 | 19, 20, 2, 10, 87, 64, 21 | dibval2 36433 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})) |
126 | 125 | adantr 481 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {(ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))})) |
127 | 108, 124,
126 | 3eltr4d 2716 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝑥 ∈ ((TEndo‘𝐾)‘𝑊) ∧ 𝑎 ∈ (𝐼‘𝑋) ∧ 𝑏 ∈ (𝐼‘𝑋))) → ((𝑥( ·𝑠
‘𝑈)𝑎)(+g‘𝑈)𝑏) ∈ (𝐼‘𝑋)) |
128 | 1, 9, 14, 15, 16, 18, 23, 24, 127 | islssd 18936 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆) |