Step | Hyp | Ref
| Expression |
1 | | lclkrlem2o.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | lclkrlem2m.y |
. . . . . . . 8
β’ (π β π β π) |
3 | 2 | snssd 4756 |
. . . . . . 7
β’ (π β {π} β π) |
4 | | lclkrlem2o.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
5 | | eqid 2736 |
. . . . . . . 8
β’
((DIsoHβπΎ)βπ) = ((DIsoHβπΎ)βπ) |
6 | | lclkrlem2o.u |
. . . . . . . 8
β’ π = ((DVecHβπΎ)βπ) |
7 | | lclkrlem2m.v |
. . . . . . . 8
β’ π = (Baseβπ) |
8 | | lclkrlem2o.o |
. . . . . . . 8
β’ β₯ =
((ocHβπΎ)βπ) |
9 | 4, 5, 6, 7, 8 | dochcl 39621 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ {π} β π) β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
10 | 1, 3, 9 | syl2anc 584 |
. . . . . 6
β’ (π β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
11 | 4, 5, 8 | dochoc 39635 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β{π})) |
12 | 1, 10, 11 | syl2anc 584 |
. . . . 5
β’ (π β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β{π})) |
13 | 12 | ad2antrr 723 |
. . . 4
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β{π})) |
14 | | lclkrlem2m.t |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
15 | | lclkrlem2m.s |
. . . . . . . . . 10
β’ π = (Scalarβπ) |
16 | | lclkrlem2m.q |
. . . . . . . . . 10
β’ Γ =
(.rβπ) |
17 | | lclkrlem2m.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
18 | | lclkrlem2m.i |
. . . . . . . . . 10
β’ πΌ = (invrβπ) |
19 | | lclkrlem2m.m |
. . . . . . . . . 10
β’ β =
(-gβπ) |
20 | | lclkrlem2m.f |
. . . . . . . . . 10
β’ πΉ = (LFnlβπ) |
21 | | lclkrlem2m.d |
. . . . . . . . . 10
β’ π· = (LDualβπ) |
22 | | lclkrlem2m.p |
. . . . . . . . . 10
β’ + =
(+gβπ·) |
23 | | lclkrlem2m.x |
. . . . . . . . . 10
β’ (π β π β π) |
24 | | lclkrlem2m.e |
. . . . . . . . . 10
β’ (π β πΈ β πΉ) |
25 | | lclkrlem2m.g |
. . . . . . . . . 10
β’ (π β πΊ β πΉ) |
26 | | lclkrlem2n.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
27 | | lclkrlem2n.l |
. . . . . . . . . 10
β’ πΏ = (LKerβπ) |
28 | | lclkrlem2o.a |
. . . . . . . . . 10
β’ β =
(LSSumβπ) |
29 | | lclkrlem2q.le |
. . . . . . . . . 10
β’ (π β (πΏβπΈ) = ( β₯ β{π})) |
30 | | lclkrlem2q.lg |
. . . . . . . . . 10
β’ (π β (πΏβπΊ) = ( β₯ β{π})) |
31 | | lclkrlem2q.b |
. . . . . . . . . 10
β’ π΅ = (π β ((((πΈ + πΊ)βπ) Γ (πΌβ((πΈ + πΊ)βπ))) Β· π)) |
32 | | lclkrlem2q.n |
. . . . . . . . . 10
β’ (π β ((πΈ + πΊ)βπ) β 0 ) |
33 | | lclkrlem2r.bn |
. . . . . . . . . 10
β’ (π β π΅ = (0gβπ)) |
34 | 7, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 2, 24, 25, 26, 27, 4, 8, 6, 28, 1,
29, 30, 31, 32, 33 | lclkrlem2r 39792 |
. . . . . . . . 9
β’ (π β (πΏβπΊ) β (πΏβ(πΈ + πΊ))) |
35 | 34 | ad2antrr 723 |
. . . . . . . 8
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β (πΏβπΊ) β (πΏβ(πΈ + πΊ))) |
36 | | eqid 2736 |
. . . . . . . . 9
β’
(LSHypβπ) =
(LSHypβπ) |
37 | 4, 6, 1 | dvhlvec 39377 |
. . . . . . . . . 10
β’ (π β π β LVec) |
38 | 37 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β π β LVec) |
39 | | simplr 766 |
. . . . . . . . 9
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β (πΏβπΊ) β (LSHypβπ)) |
40 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β (πΏβ(πΈ + πΊ)) β (LSHypβπ)) |
41 | 36, 38, 39, 40 | lshpcmp 37255 |
. . . . . . . 8
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β ((πΏβπΊ) β (πΏβ(πΈ + πΊ)) β (πΏβπΊ) = (πΏβ(πΈ + πΊ)))) |
42 | 35, 41 | mpbid 231 |
. . . . . . 7
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β (πΏβπΊ) = (πΏβ(πΈ + πΊ))) |
43 | 30 | ad2antrr 723 |
. . . . . . 7
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β (πΏβπΊ) = ( β₯ β{π})) |
44 | 42, 43 | eqtr3d 2778 |
. . . . . 6
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β (πΏβ(πΈ + πΊ)) = ( β₯ β{π})) |
45 | 44 | fveq2d 6829 |
. . . . 5
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β ( β₯ β(πΏβ(πΈ + πΊ))) = ( β₯ β( β₯
β{π}))) |
46 | 45 | fveq2d 6829 |
. . . 4
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = ( β₯ β( β₯
β( β₯ β{π})))) |
47 | 13, 46, 44 | 3eqtr4d 2786 |
. . 3
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) β (LSHypβπ)) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) |
48 | 4, 6, 8, 7, 1 | dochoc1 39629 |
. . . . 5
β’ (π β ( β₯ β( β₯
βπ)) = π) |
49 | 48 | ad2antrr 723 |
. . . 4
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) = π) β ( β₯ β( β₯
βπ)) = π) |
50 | | simpr 485 |
. . . . . 6
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) = π) β (πΏβ(πΈ + πΊ)) = π) |
51 | 50 | fveq2d 6829 |
. . . . 5
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) = π) β ( β₯ β(πΏβ(πΈ + πΊ))) = ( β₯ βπ)) |
52 | 51 | fveq2d 6829 |
. . . 4
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) = π) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = ( β₯ β( β₯
βπ))) |
53 | 49, 52, 50 | 3eqtr4d 2786 |
. . 3
β’ (((π β§ (πΏβπΊ) β (LSHypβπ)) β§ (πΏβ(πΈ + πΊ)) = π) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) |
54 | 4, 6, 1 | dvhlmod 39378 |
. . . . . 6
β’ (π β π β LMod) |
55 | 20, 21, 22, 54, 24, 25 | ldualvaddcl 37397 |
. . . . 5
β’ (π β (πΈ + πΊ) β πΉ) |
56 | 7, 36, 20, 27, 37, 55 | lkrshpor 37374 |
. . . 4
β’ (π β ((πΏβ(πΈ + πΊ)) β (LSHypβπ) β¨ (πΏβ(πΈ + πΊ)) = π)) |
57 | 56 | adantr 481 |
. . 3
β’ ((π β§ (πΏβπΊ) β (LSHypβπ)) β ((πΏβ(πΈ + πΊ)) β (LSHypβπ) β¨ (πΏβ(πΈ + πΊ)) = π)) |
58 | 47, 53, 57 | mpjaodan 956 |
. 2
β’ ((π β§ (πΏβπΊ) β (LSHypβπ)) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) |
59 | 48 | adantr 481 |
. . 3
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β( β₯
βπ)) = π) |
60 | 7, 20, 27, 54, 55 | lkrssv 37363 |
. . . . . . 7
β’ (π β (πΏβ(πΈ + πΊ)) β π) |
61 | 60 | adantr 481 |
. . . . . 6
β’ ((π β§ (πΏβπΊ) = π) β (πΏβ(πΈ + πΊ)) β π) |
62 | | simpr 485 |
. . . . . . 7
β’ ((π β§ (πΏβπΊ) = π) β (πΏβπΊ) = π) |
63 | 34 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πΏβπΊ) = π) β (πΏβπΊ) β (πΏβ(πΈ + πΊ))) |
64 | 62, 63 | eqsstrrd 3971 |
. . . . . 6
β’ ((π β§ (πΏβπΊ) = π) β π β (πΏβ(πΈ + πΊ))) |
65 | 61, 64 | eqssd 3949 |
. . . . 5
β’ ((π β§ (πΏβπΊ) = π) β (πΏβ(πΈ + πΊ)) = π) |
66 | 65 | fveq2d 6829 |
. . . 4
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β(πΏβ(πΈ + πΊ))) = ( β₯ βπ)) |
67 | 66 | fveq2d 6829 |
. . 3
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = ( β₯ β( β₯
βπ))) |
68 | 59, 67, 65 | 3eqtr4d 2786 |
. 2
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) |
69 | 7, 36, 20, 27, 37, 25 | lkrshpor 37374 |
. 2
β’ (π β ((πΏβπΊ) β (LSHypβπ) β¨ (πΏβπΊ) = π)) |
70 | 58, 68, 69 | mpjaodan 956 |
1
β’ (π β ( β₯ β( β₯
β(πΏβ(πΈ + πΊ)))) = (πΏβ(πΈ + πΊ))) |