Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
2 | 1 | lindff 21237 |
. . . 4
β’ ((πΉ LIndF π β§ π β LMod) β πΉ:dom πΉβΆ(Baseβπ)) |
3 | 2 | ancoms 460 |
. . 3
β’ ((π β LMod β§ πΉ LIndF π) β πΉ:dom πΉβΆ(Baseβπ)) |
4 | 3 | frnd 6681 |
. 2
β’ ((π β LMod β§ πΉ LIndF π) β ran πΉ β (Baseβπ)) |
5 | | simpll 766 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π) β§ π¦ β dom πΉ) β π β LMod) |
6 | | imassrn 6029 |
. . . . . . . . 9
β’ (πΉ β (dom πΉ β {π¦})) β ran πΉ |
7 | 6, 4 | sstrid 3960 |
. . . . . . . 8
β’ ((π β LMod β§ πΉ LIndF π) β (πΉ β (dom πΉ β {π¦})) β (Baseβπ)) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π) β§ π¦ β dom πΉ) β (πΉ β (dom πΉ β {π¦})) β (Baseβπ)) |
9 | 3 | ffund 6677 |
. . . . . . . 8
β’ ((π β LMod β§ πΉ LIndF π) β Fun πΉ) |
10 | | eldifsn 4752 |
. . . . . . . . . 10
β’ (π₯ β (ran πΉ β {(πΉβπ¦)}) β (π₯ β ran πΉ β§ π₯ β (πΉβπ¦))) |
11 | | funfn 6536 |
. . . . . . . . . . . . . 14
β’ (Fun
πΉ β πΉ Fn dom πΉ) |
12 | | fvelrnb 6908 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn dom πΉ β (π₯ β ran πΉ β βπ β dom πΉ(πΉβπ) = π₯)) |
13 | 11, 12 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (Fun
πΉ β (π₯ β ran πΉ β βπ β dom πΉ(πΉβπ) = π₯)) |
14 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β (π₯ β ran πΉ β βπ β dom πΉ(πΉβπ) = π₯)) |
15 | | difss 4096 |
. . . . . . . . . . . . . . . . . 18
β’ (dom
πΉ β {π¦}) β dom πΉ |
16 | 15 | jctr 526 |
. . . . . . . . . . . . . . . . 17
β’ (Fun
πΉ β (Fun πΉ β§ (dom πΉ β {π¦}) β dom πΉ)) |
17 | 16 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((Fun
πΉ β§ π¦ β dom πΉ) β§ (π β dom πΉ β§ (πΉβπ) β (πΉβπ¦))) β (Fun πΉ β§ (dom πΉ β {π¦}) β dom πΉ)) |
18 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom πΉ β§ (πΉβπ) β (πΉβπ¦)) β π β dom πΉ) |
19 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π¦ β (πΉβπ) = (πΉβπ¦)) |
20 | 19 | necon3i 2977 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) β (πΉβπ¦) β π β π¦) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom πΉ β§ (πΉβπ) β (πΉβπ¦)) β π β π¦) |
22 | | eldifsn 4752 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (dom πΉ β {π¦}) β (π β dom πΉ β§ π β π¦)) |
23 | 18, 21, 22 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom πΉ β§ (πΉβπ) β (πΉβπ¦)) β π β (dom πΉ β {π¦})) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((Fun
πΉ β§ π¦ β dom πΉ) β§ (π β dom πΉ β§ (πΉβπ) β (πΉβπ¦))) β π β (dom πΉ β {π¦})) |
25 | | funfvima2 7186 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
πΉ β§ (dom πΉ β {π¦}) β dom πΉ) β (π β (dom πΉ β {π¦}) β (πΉβπ) β (πΉ β (dom πΉ β {π¦})))) |
26 | 17, 24, 25 | sylc 65 |
. . . . . . . . . . . . . . 15
β’ (((Fun
πΉ β§ π¦ β dom πΉ) β§ (π β dom πΉ β§ (πΉβπ) β (πΉβπ¦))) β (πΉβπ) β (πΉ β (dom πΉ β {π¦}))) |
27 | 26 | expr 458 |
. . . . . . . . . . . . . 14
β’ (((Fun
πΉ β§ π¦ β dom πΉ) β§ π β dom πΉ) β ((πΉβπ) β (πΉβπ¦) β (πΉβπ) β (πΉ β (dom πΉ β {π¦})))) |
28 | | neeq1 3007 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) = π₯ β ((πΉβπ) β (πΉβπ¦) β π₯ β (πΉβπ¦))) |
29 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) = π₯ β ((πΉβπ) β (πΉ β (dom πΉ β {π¦})) β π₯ β (πΉ β (dom πΉ β {π¦})))) |
30 | 28, 29 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) = π₯ β (((πΉβπ) β (πΉβπ¦) β (πΉβπ) β (πΉ β (dom πΉ β {π¦}))) β (π₯ β (πΉβπ¦) β π₯ β (πΉ β (dom πΉ β {π¦}))))) |
31 | 27, 30 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (((Fun
πΉ β§ π¦ β dom πΉ) β§ π β dom πΉ) β ((πΉβπ) = π₯ β (π₯ β (πΉβπ¦) β π₯ β (πΉ β (dom πΉ β {π¦}))))) |
32 | 31 | rexlimdva 3153 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β (βπ β dom πΉ(πΉβπ) = π₯ β (π₯ β (πΉβπ¦) β π₯ β (πΉ β (dom πΉ β {π¦}))))) |
33 | 14, 32 | sylbid 239 |
. . . . . . . . . . 11
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β (π₯ β ran πΉ β (π₯ β (πΉβπ¦) β π₯ β (πΉ β (dom πΉ β {π¦}))))) |
34 | 33 | impd 412 |
. . . . . . . . . 10
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β ((π₯ β ran πΉ β§ π₯ β (πΉβπ¦)) β π₯ β (πΉ β (dom πΉ β {π¦})))) |
35 | 10, 34 | biimtrid 241 |
. . . . . . . . 9
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β (π₯ β (ran πΉ β {(πΉβπ¦)}) β π₯ β (πΉ β (dom πΉ β {π¦})))) |
36 | 35 | ssrdv 3955 |
. . . . . . . 8
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β (ran πΉ β {(πΉβπ¦)}) β (πΉ β (dom πΉ β {π¦}))) |
37 | 9, 36 | sylan 581 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π) β§ π¦ β dom πΉ) β (ran πΉ β {(πΉβπ¦)}) β (πΉ β (dom πΉ β {π¦}))) |
38 | | eqid 2737 |
. . . . . . . 8
β’
(LSpanβπ) =
(LSpanβπ) |
39 | 1, 38 | lspss 20461 |
. . . . . . 7
β’ ((π β LMod β§ (πΉ β (dom πΉ β {π¦})) β (Baseβπ) β§ (ran πΉ β {(πΉβπ¦)}) β (πΉ β (dom πΉ β {π¦}))) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})) β ((LSpanβπ)β(πΉ β (dom πΉ β {π¦})))) |
40 | 5, 8, 37, 39 | syl3anc 1372 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π) β§ π¦ β dom πΉ) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})) β ((LSpanβπ)β(πΉ β (dom πΉ β {π¦})))) |
41 | 40 | adantrr 716 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})) β ((LSpanβπ)β(πΉ β (dom πΉ β {π¦})))) |
42 | | simplr 768 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β πΉ LIndF π) |
43 | | simprl 770 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π¦ β dom πΉ) |
44 | | eldifi 4091 |
. . . . . . 7
β’ (π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β π β (Baseβ(Scalarβπ))) |
45 | 44 | ad2antll 728 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π β (Baseβ(Scalarβπ))) |
46 | | eldifsni 4755 |
. . . . . . 7
β’ (π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β π β
(0gβ(Scalarβπ))) |
47 | 46 | ad2antll 728 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π β
(0gβ(Scalarβπ))) |
48 | | eqid 2737 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
49 | | eqid 2737 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
50 | | eqid 2737 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
51 | | eqid 2737 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
52 | 48, 38, 49, 50, 51 | lindfind 21238 |
. . . . . 6
β’ (((πΉ LIndF π β§ π¦ β dom πΉ) β§ (π β (Baseβ(Scalarβπ)) β§ π β
(0gβ(Scalarβπ)))) β Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(πΉ β (dom πΉ β {π¦})))) |
53 | 42, 43, 45, 47, 52 | syl22anc 838 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(πΉ β (dom πΉ β {π¦})))) |
54 | 41, 53 | ssneldd 3952 |
. . . 4
β’ (((π β LMod β§ πΉ LIndF π) β§ (π¦ β dom πΉ β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)}))) |
55 | 54 | ralrimivva 3198 |
. . 3
β’ ((π β LMod β§ πΉ LIndF π) β βπ¦ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)}))) |
56 | 9 | funfnd 6537 |
. . . 4
β’ ((π β LMod β§ πΉ LIndF π) β πΉ Fn dom πΉ) |
57 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = (πΉβπ¦) β (π( Β·π
βπ)π₯) = (π( Β·π
βπ)(πΉβπ¦))) |
58 | | sneq 4601 |
. . . . . . . . . 10
β’ (π₯ = (πΉβπ¦) β {π₯} = {(πΉβπ¦)}) |
59 | 58 | difeq2d 4087 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ¦) β (ran πΉ β {π₯}) = (ran πΉ β {(πΉβπ¦)})) |
60 | 59 | fveq2d 6851 |
. . . . . . . 8
β’ (π₯ = (πΉβπ¦) β ((LSpanβπ)β(ran πΉ β {π₯})) = ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)}))) |
61 | 57, 60 | eleq12d 2832 |
. . . . . . 7
β’ (π₯ = (πΉβπ¦) β ((π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯})) β (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})))) |
62 | 61 | notbid 318 |
. . . . . 6
β’ (π₯ = (πΉβπ¦) β (Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯})) β Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})))) |
63 | 62 | ralbidv 3175 |
. . . . 5
β’ (π₯ = (πΉβπ¦) β (βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯})) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})))) |
64 | 63 | ralrn 7043 |
. . . 4
β’ (πΉ Fn dom πΉ β (βπ₯ β ran πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯})) β βπ¦ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})))) |
65 | 56, 64 | syl 17 |
. . 3
β’ ((π β LMod β§ πΉ LIndF π) β (βπ₯ β ran πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯})) β βπ¦ β dom πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ¦)) β ((LSpanβπ)β(ran πΉ β {(πΉβπ¦)})))) |
66 | 55, 65 | mpbird 257 |
. 2
β’ ((π β LMod β§ πΉ LIndF π) β βπ₯ β ran πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯}))) |
67 | 1, 48, 38, 49, 51, 50 | islinds2 21235 |
. . 3
β’ (π β LMod β (ran πΉ β (LIndSβπ) β (ran πΉ β (Baseβπ) β§ βπ₯ β ran πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯}))))) |
68 | 67 | adantr 482 |
. 2
β’ ((π β LMod β§ πΉ LIndF π) β (ran πΉ β (LIndSβπ) β (ran πΉ β (Baseβπ) β§ βπ₯ β ran πΉβπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)π₯) β ((LSpanβπ)β(ran πΉ β {π₯}))))) |
69 | 4, 66, 68 | mpbir2and 712 |
1
β’ ((π β LMod β§ πΉ LIndF π) β ran πΉ β (LIndSβπ)) |