Step | Hyp | Ref
| Expression |
1 | | lfl1dim.w |
. . . . . . . . 9
β’ (π β π β LVec) |
2 | | lveclmod 20716 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
4 | | lfl1dim.d |
. . . . . . . . 9
β’ π· = (Scalarβπ) |
5 | | lfl1dim.k |
. . . . . . . . 9
β’ πΎ = (Baseβπ·) |
6 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπ·) = (0gβπ·) |
7 | 4, 5, 6 | lmod0cl 20497 |
. . . . . . . 8
β’ (π β LMod β
(0gβπ·)
β πΎ) |
8 | 3, 7 | syl 17 |
. . . . . . 7
β’ (π β (0gβπ·) β πΎ) |
9 | 8 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β
(0gβπ·)
β πΎ) |
10 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β π = (π Γ {(0gβπ·)})) |
11 | | lfl1dim.v |
. . . . . . . 8
β’ π = (Baseβπ) |
12 | | lfl1dim.f |
. . . . . . . 8
β’ πΉ = (LFnlβπ) |
13 | | lfl1dim.t |
. . . . . . . 8
β’ Β· =
(.rβπ·) |
14 | 3 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β π β LMod) |
15 | | lfl1dim.g |
. . . . . . . . 9
β’ (π β πΊ β πΉ) |
16 | 15 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β πΊ β πΉ) |
17 | 11, 4, 12, 5, 13, 6, 14, 16 | lfl0sc 37947 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β (πΊ βf Β· (π Γ {(0gβπ·)})) = (π Γ {(0gβπ·)})) |
18 | 10, 17 | eqtr4d 2775 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β π = (πΊ βf Β· (π Γ {(0gβπ·)}))) |
19 | | sneq 4638 |
. . . . . . . . 9
β’ (π = (0gβπ·) β {π} = {(0gβπ·)}) |
20 | 19 | xpeq2d 5706 |
. . . . . . . 8
β’ (π = (0gβπ·) β (π Γ {π}) = (π Γ {(0gβπ·)})) |
21 | 20 | oveq2d 7424 |
. . . . . . 7
β’ (π = (0gβπ·) β (πΊ βf Β· (π Γ {π})) = (πΊ βf Β· (π Γ {(0gβπ·)}))) |
22 | 21 | rspceeqv 3633 |
. . . . . 6
β’
(((0gβπ·) β πΎ β§ π = (πΊ βf Β· (π Γ {(0gβπ·)}))) β βπ β πΎ π = (πΊ βf Β· (π Γ {π}))) |
23 | 9, 18, 22 | syl2anc 584 |
. . . . 5
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β βπ β πΎ π = (πΊ βf Β· (π Γ {π}))) |
24 | 23 | a1d 25 |
. . . 4
β’ (((π β§ π β πΉ) β§ π = (π Γ {(0gβπ·)})) β ((πΏβπΊ) β (πΏβπ) β βπ β πΎ π = (πΊ βf Β· (π Γ {π})))) |
25 | 8 | ad3antrrr 728 |
. . . . . 6
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β (0gβπ·) β πΎ) |
26 | | lfl1dim.l |
. . . . . . . . . 10
β’ πΏ = (LKerβπ) |
27 | 3 | ad3antrrr 728 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β π β LMod) |
28 | | simpllr 774 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β π β πΉ) |
29 | 11, 12, 26, 27, 28 | lkrssv 37961 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β (πΏβπ) β π) |
30 | 3 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΉ) β π β LMod) |
31 | 15 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΉ) β πΊ β πΉ) |
32 | 4, 6, 11, 12, 26 | lkr0f 37959 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ πΊ β πΉ) β ((πΏβπΊ) = π β πΊ = (π Γ {(0gβπ·)}))) |
33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΉ) β ((πΏβπΊ) = π β πΊ = (π Γ {(0gβπ·)}))) |
34 | 33 | biimpar 478 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β (πΏβπΊ) = π) |
35 | 34 | sseq1d 4013 |
. . . . . . . . . 10
β’ (((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β ((πΏβπΊ) β (πΏβπ) β π β (πΏβπ))) |
36 | 35 | biimpa 477 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β π β (πΏβπ)) |
37 | 29, 36 | eqssd 3999 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β (πΏβπ) = π) |
38 | 4, 6, 11, 12, 26 | lkr0f 37959 |
. . . . . . . . 9
β’ ((π β LMod β§ π β πΉ) β ((πΏβπ) = π β π = (π Γ {(0gβπ·)}))) |
39 | 27, 28, 38 | syl2anc 584 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β ((πΏβπ) = π β π = (π Γ {(0gβπ·)}))) |
40 | 37, 39 | mpbid 231 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β π = (π Γ {(0gβπ·)})) |
41 | 15 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β πΊ β πΉ) |
42 | 11, 4, 12, 5, 13, 6, 27, 41 | lfl0sc 37947 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β (πΊ βf Β· (π Γ {(0gβπ·)})) = (π Γ {(0gβπ·)})) |
43 | 40, 42 | eqtr4d 2775 |
. . . . . 6
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β π = (πΊ βf Β· (π Γ {(0gβπ·)}))) |
44 | 25, 43, 22 | syl2anc 584 |
. . . . 5
β’ ((((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β§ (πΏβπΊ) β (πΏβπ)) β βπ β πΎ π = (πΊ βf Β· (π Γ {π}))) |
45 | 44 | ex 413 |
. . . 4
β’ (((π β§ π β πΉ) β§ πΊ = (π Γ {(0gβπ·)})) β ((πΏβπΊ) β (πΏβπ) β βπ β πΎ π = (πΊ βf Β· (π Γ {π})))) |
46 | | eqid 2732 |
. . . . . 6
β’
(LSHypβπ) =
(LSHypβπ) |
47 | 1 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β π β LVec) |
48 | 15 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β πΊ β πΉ) |
49 | | simprr 771 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β πΊ β (π Γ {(0gβπ·)})) |
50 | 11, 4, 6, 46, 12, 26 | lkrshp 37970 |
. . . . . . 7
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ {(0gβπ·)})) β (πΏβπΊ) β (LSHypβπ)) |
51 | 47, 48, 49, 50 | syl3anc 1371 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β (πΏβπΊ) β (LSHypβπ)) |
52 | | simplr 767 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β π β πΉ) |
53 | | simprl 769 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β π β (π Γ {(0gβπ·)})) |
54 | 11, 4, 6, 46, 12, 26 | lkrshp 37970 |
. . . . . . 7
β’ ((π β LVec β§ π β πΉ β§ π β (π Γ {(0gβπ·)})) β (πΏβπ) β (LSHypβπ)) |
55 | 47, 52, 53, 54 | syl3anc 1371 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β (πΏβπ) β (LSHypβπ)) |
56 | 46, 47, 51, 55 | lshpcmp 37853 |
. . . . 5
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β ((πΏβπΊ) β (πΏβπ) β (πΏβπΊ) = (πΏβπ))) |
57 | 1 | ad3antrrr 728 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β§ (πΏβπΊ) = (πΏβπ)) β π β LVec) |
58 | 15 | ad3antrrr 728 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β§ (πΏβπΊ) = (πΏβπ)) β πΊ β πΉ) |
59 | | simpllr 774 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β§ (πΏβπΊ) = (πΏβπ)) β π β πΉ) |
60 | | simpr 485 |
. . . . . . 7
β’ ((((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β§ (πΏβπΊ) = (πΏβπ)) β (πΏβπΊ) = (πΏβπ)) |
61 | 4, 5, 13, 11, 12, 26 | eqlkr2 37965 |
. . . . . . 7
β’ ((π β LVec β§ (πΊ β πΉ β§ π β πΉ) β§ (πΏβπΊ) = (πΏβπ)) β βπ β πΎ π = (πΊ βf Β· (π Γ {π}))) |
62 | 57, 58, 59, 60, 61 | syl121anc 1375 |
. . . . . 6
β’ ((((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β§ (πΏβπΊ) = (πΏβπ)) β βπ β πΎ π = (πΊ βf Β· (π Γ {π}))) |
63 | 62 | ex 413 |
. . . . 5
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β ((πΏβπΊ) = (πΏβπ) β βπ β πΎ π = (πΊ βf Β· (π Γ {π})))) |
64 | 56, 63 | sylbid 239 |
. . . 4
β’ (((π β§ π β πΉ) β§ (π β (π Γ {(0gβπ·)}) β§ πΊ β (π Γ {(0gβπ·)}))) β ((πΏβπΊ) β (πΏβπ) β βπ β πΎ π = (πΊ βf Β· (π Γ {π})))) |
65 | 24, 45, 64 | pm2.61da2ne 3030 |
. . 3
β’ ((π β§ π β πΉ) β ((πΏβπΊ) β (πΏβπ) β βπ β πΎ π = (πΊ βf Β· (π Γ {π})))) |
66 | 1 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ π β πΎ) β π β LVec) |
67 | 15 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ π β πΎ) β πΊ β πΉ) |
68 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ π β πΎ) β π β πΎ) |
69 | 11, 4, 5, 13, 12, 26, 66, 67, 68 | lkrscss 37963 |
. . . . . 6
β’ (((π β§ π β πΉ) β§ π β πΎ) β (πΏβπΊ) β (πΏβ(πΊ βf Β· (π Γ {π})))) |
70 | 69 | ex 413 |
. . . . 5
β’ ((π β§ π β πΉ) β (π β πΎ β (πΏβπΊ) β (πΏβ(πΊ βf Β· (π Γ {π}))))) |
71 | | fveq2 6891 |
. . . . . . 7
β’ (π = (πΊ βf Β· (π Γ {π})) β (πΏβπ) = (πΏβ(πΊ βf Β· (π Γ {π})))) |
72 | 71 | sseq2d 4014 |
. . . . . 6
β’ (π = (πΊ βf Β· (π Γ {π})) β ((πΏβπΊ) β (πΏβπ) β (πΏβπΊ) β (πΏβ(πΊ βf Β· (π Γ {π}))))) |
73 | 72 | biimprcd 249 |
. . . . 5
β’ ((πΏβπΊ) β (πΏβ(πΊ βf Β· (π Γ {π}))) β (π = (πΊ βf Β· (π Γ {π})) β (πΏβπΊ) β (πΏβπ))) |
74 | 70, 73 | syl6 35 |
. . . 4
β’ ((π β§ π β πΉ) β (π β πΎ β (π = (πΊ βf Β· (π Γ {π})) β (πΏβπΊ) β (πΏβπ)))) |
75 | 74 | rexlimdv 3153 |
. . 3
β’ ((π β§ π β πΉ) β (βπ β πΎ π = (πΊ βf Β· (π Γ {π})) β (πΏβπΊ) β (πΏβπ))) |
76 | 65, 75 | impbid 211 |
. 2
β’ ((π β§ π β πΉ) β ((πΏβπΊ) β (πΏβπ) β βπ β πΎ π = (πΊ βf Β· (π Γ {π})))) |
77 | 76 | rabbidva 3439 |
1
β’ (π β {π β πΉ β£ (πΏβπΊ) β (πΏβπ)} = {π β πΉ β£ βπ β πΎ π = (πΊ βf Β· (π Γ {π}))}) |