Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
2 | 1 | lindff 21370 |
. . . . . 6
β’ ((πΉ LIndF π β§ π β LMod) β πΉ:dom πΉβΆ(Baseβπ)) |
3 | 2 | ancoms 460 |
. . . . 5
β’ ((π β LMod β§ πΉ LIndF π) β πΉ:dom πΉβΆ(Baseβπ)) |
4 | 3 | 3adant3 1133 |
. . . 4
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΉ:dom πΉβΆ(Baseβπ)) |
5 | | f1f 6788 |
. . . . 5
β’ (πΊ:πΎβ1-1βdom πΉ β πΊ:πΎβΆdom πΉ) |
6 | 5 | 3ad2ant3 1136 |
. . . 4
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΊ:πΎβΆdom πΉ) |
7 | | fco 6742 |
. . . 4
β’ ((πΉ:dom πΉβΆ(Baseβπ) β§ πΊ:πΎβΆdom πΉ) β (πΉ β πΊ):πΎβΆ(Baseβπ)) |
8 | 4, 6, 7 | syl2anc 585 |
. . 3
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΉ β πΊ):πΎβΆ(Baseβπ)) |
9 | 8 | ffdmd 6749 |
. 2
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΉ β πΊ):dom (πΉ β πΊ)βΆ(Baseβπ)) |
10 | | simpl2 1193 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β πΉ LIndF π) |
11 | 6 | adantr 482 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β πΊ:πΎβΆdom πΉ) |
12 | 8 | fdmd 6729 |
. . . . . . . . 9
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β dom (πΉ β πΊ) = πΎ) |
13 | 12 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (π₯ β dom (πΉ β πΊ) β π₯ β πΎ)) |
14 | 13 | biimpa 478 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β π₯ β πΎ) |
15 | 11, 14 | ffvelcdmd 7088 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β (πΊβπ₯) β dom πΉ) |
16 | 15 | adantrr 716 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (πΊβπ₯) β dom πΉ) |
17 | | eldifi 4127 |
. . . . . 6
β’ (π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β π β (Baseβ(Scalarβπ))) |
18 | 17 | ad2antll 728 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π β (Baseβ(Scalarβπ))) |
19 | | eldifsni 4794 |
. . . . . 6
β’ (π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β π β
(0gβ(Scalarβπ))) |
20 | 19 | ad2antll 728 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π β
(0gβ(Scalarβπ))) |
21 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
22 | | eqid 2733 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
23 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
24 | | eqid 2733 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
25 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
26 | 21, 22, 23, 24, 25 | lindfind 21371 |
. . . . 5
β’ (((πΉ LIndF π β§ (πΊβπ₯) β dom πΉ) β§ (π β (Baseβ(Scalarβπ)) β§ π β
(0gβ(Scalarβπ)))) β Β¬ (π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)})))) |
27 | 10, 16, 18, 20, 26 | syl22anc 838 |
. . . 4
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ (π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)})))) |
28 | | f1fn 6789 |
. . . . . . . . . . 11
β’ (πΊ:πΎβ1-1βdom πΉ β πΊ Fn πΎ) |
29 | 28 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΊ Fn πΎ) |
30 | 29 | adantr 482 |
. . . . . . . . 9
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β πΊ Fn πΎ) |
31 | | fvco2 6989 |
. . . . . . . . 9
β’ ((πΊ Fn πΎ β§ π₯ β πΎ) β ((πΉ β πΊ)βπ₯) = (πΉβ(πΊβπ₯))) |
32 | 30, 14, 31 | syl2anc 585 |
. . . . . . . 8
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β ((πΉ β πΊ)βπ₯) = (πΉβ(πΊβπ₯))) |
33 | 32 | oveq2d 7425 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β (π( Β·π
βπ)((πΉ β πΊ)βπ₯)) = (π( Β·π
βπ)(πΉβ(πΊβπ₯)))) |
34 | 33 | eleq1d 2819 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β ((π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β (π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))))) |
35 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β π β LMod) |
36 | | imassrn 6071 |
. . . . . . . . . . 11
β’ (πΉ β (dom πΉ β {(πΊβπ₯)})) β ran πΉ |
37 | 4 | frnd 6726 |
. . . . . . . . . . 11
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β ran πΉ β (Baseβπ)) |
38 | 36, 37 | sstrid 3994 |
. . . . . . . . . 10
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΉ β (dom πΉ β {(πΊβπ₯)})) β (Baseβπ)) |
39 | 38 | adantr 482 |
. . . . . . . . 9
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β (πΉ β (dom πΉ β {(πΊβπ₯)})) β (Baseβπ)) |
40 | | imaco 6251 |
. . . . . . . . . 10
β’ ((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})) = (πΉ β (πΊ β (dom (πΉ β πΊ) β {π₯}))) |
41 | 12 | difeq1d 4122 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (dom (πΉ β πΊ) β {π₯}) = (πΎ β {π₯})) |
42 | 41 | imaeq2d 6060 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΊ β (dom (πΉ β πΊ) β {π₯})) = (πΊ β (πΎ β {π₯}))) |
43 | | df-f1 6549 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ:πΎβ1-1βdom πΉ β (πΊ:πΎβΆdom πΉ β§ Fun β‘πΊ)) |
44 | 43 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’ (πΊ:πΎβ1-1βdom πΉ β Fun β‘πΊ) |
45 | 44 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β Fun β‘πΊ) |
46 | | imadif 6633 |
. . . . . . . . . . . . . . 15
β’ (Fun
β‘πΊ β (πΊ β (πΎ β {π₯})) = ((πΊ β πΎ) β (πΊ β {π₯}))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΊ β (πΎ β {π₯})) = ((πΊ β πΎ) β (πΊ β {π₯}))) |
48 | 42, 47 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΊ β (dom (πΉ β πΊ) β {π₯})) = ((πΊ β πΎ) β (πΊ β {π₯}))) |
49 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β (πΊ β (dom (πΉ β πΊ) β {π₯})) = ((πΊ β πΎ) β (πΊ β {π₯}))) |
50 | | fnsnfv 6971 |
. . . . . . . . . . . . . . 15
β’ ((πΊ Fn πΎ β§ π₯ β πΎ) β {(πΊβπ₯)} = (πΊ β {π₯})) |
51 | 29, 50 | sylan 581 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β {(πΊβπ₯)} = (πΊ β {π₯})) |
52 | 51 | difeq2d 4123 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β ((πΊ β πΎ) β {(πΊβπ₯)}) = ((πΊ β πΎ) β (πΊ β {π₯}))) |
53 | | imassrn 6071 |
. . . . . . . . . . . . . . 15
β’ (πΊ β πΎ) β ran πΊ |
54 | 6 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β πΊ:πΎβΆdom πΉ) |
55 | 54 | frnd 6726 |
. . . . . . . . . . . . . . 15
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β ran πΊ β dom πΉ) |
56 | 53, 55 | sstrid 3994 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β (πΊ β πΎ) β dom πΉ) |
57 | 56 | ssdifd 4141 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β ((πΊ β πΎ) β {(πΊβπ₯)}) β (dom πΉ β {(πΊβπ₯)})) |
58 | 52, 57 | eqsstrrd 4022 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β ((πΊ β πΎ) β (πΊ β {π₯})) β (dom πΉ β {(πΊβπ₯)})) |
59 | 49, 58 | eqsstrd 4021 |
. . . . . . . . . . 11
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β (πΊ β (dom (πΉ β πΊ) β {π₯})) β (dom πΉ β {(πΊβπ₯)})) |
60 | | imass2 6102 |
. . . . . . . . . . 11
β’ ((πΊ β (dom (πΉ β πΊ) β {π₯})) β (dom πΉ β {(πΊβπ₯)}) β (πΉ β (πΊ β (dom (πΉ β πΊ) β {π₯}))) β (πΉ β (dom πΉ β {(πΊβπ₯)}))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . 10
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β (πΉ β (πΊ β (dom (πΉ β πΊ) β {π₯}))) β (πΉ β (dom πΉ β {(πΊβπ₯)}))) |
62 | 40, 61 | eqsstrid 4031 |
. . . . . . . . 9
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β ((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})) β (πΉ β (dom πΉ β {(πΊβπ₯)}))) |
63 | 1, 22 | lspss 20595 |
. . . . . . . . 9
β’ ((π β LMod β§ (πΉ β (dom πΉ β {(πΊβπ₯)})) β (Baseβπ) β§ ((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})) β (πΉ β (dom πΉ β {(πΊβπ₯)}))) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)})))) |
64 | 35, 39, 62, 63 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β πΎ) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)})))) |
65 | 14, 64 | syldan 592 |
. . . . . . 7
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)})))) |
66 | 65 | sseld 3982 |
. . . . . 6
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β ((π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β (π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)}))))) |
67 | 34, 66 | sylbid 239 |
. . . . 5
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ π₯ β dom (πΉ β πΊ)) β ((π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β (π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)}))))) |
68 | 67 | adantrr 716 |
. . . 4
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β ((π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯}))) β (π( Β·π
βπ)(πΉβ(πΊβπ₯))) β ((LSpanβπ)β(πΉ β (dom πΉ β {(πΊβπ₯)}))))) |
69 | 27, 68 | mtod 197 |
. . 3
β’ (((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β§ (π₯ β dom (πΉ β πΊ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ (π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})))) |
70 | 69 | ralrimivva 3201 |
. 2
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β βπ₯ β dom (πΉ β πΊ)βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})))) |
71 | | simp1 1137 |
. . 3
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β π β LMod) |
72 | | rellindf 21363 |
. . . . . 6
β’ Rel
LIndF |
73 | 72 | brrelex1i 5733 |
. . . . 5
β’ (πΉ LIndF π β πΉ β V) |
74 | 73 | 3ad2ant2 1135 |
. . . 4
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΉ β V) |
75 | | simp3 1139 |
. . . . . 6
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΊ:πΎβ1-1βdom πΉ) |
76 | 74 | dmexd 7896 |
. . . . . 6
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β dom πΉ β V) |
77 | | f1dmex 7943 |
. . . . . 6
β’ ((πΊ:πΎβ1-1βdom πΉ β§ dom πΉ β V) β πΎ β V) |
78 | 75, 76, 77 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΎ β V) |
79 | 6, 78 | fexd 7229 |
. . . 4
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β πΊ β V) |
80 | | coexg 7920 |
. . . 4
β’ ((πΉ β V β§ πΊ β V) β (πΉ β πΊ) β V) |
81 | 74, 79, 80 | syl2anc 585 |
. . 3
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΉ β πΊ) β V) |
82 | 1, 21, 22, 23, 25, 24 | islindf 21367 |
. . 3
β’ ((π β LMod β§ (πΉ β πΊ) β V) β ((πΉ β πΊ) LIndF π β ((πΉ β πΊ):dom (πΉ β πΊ)βΆ(Baseβπ) β§ βπ₯ β dom (πΉ β πΊ)βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})))))) |
83 | 71, 81, 82 | syl2anc 585 |
. 2
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β ((πΉ β πΊ) LIndF π β ((πΉ β πΊ):dom (πΉ β πΊ)βΆ(Baseβπ) β§ βπ₯ β dom (πΉ β πΊ)βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΉ β πΊ)βπ₯)) β ((LSpanβπ)β((πΉ β πΊ) β (dom (πΉ β πΊ) β {π₯})))))) |
84 | 9, 70, 83 | mpbir2and 712 |
1
β’ ((π β LMod β§ πΉ LIndF π β§ πΊ:πΎβ1-1βdom πΉ) β (πΉ β πΊ) LIndF π) |