Step | Hyp | Ref
| Expression |
1 | | rellindf 21354 |
. . . . 5
β’ Rel
LIndF |
2 | 1 | brrelex1i 5730 |
. . . 4
β’ (πΉ LIndF π β πΉ β V) |
3 | | simp3 1138 |
. . . 4
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β πΉ:πΌβΆπ΅) |
4 | | dmfex 7894 |
. . . 4
β’ ((πΉ β V β§ πΉ:πΌβΆπ΅) β πΌ β V) |
5 | 2, 3, 4 | syl2anr 597 |
. . 3
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β§ πΉ LIndF π) β πΌ β V) |
6 | 5 | ex 413 |
. 2
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β πΌ β V)) |
7 | 1 | brrelex1i 5730 |
. . . 4
β’ ((πΊ β πΉ) LIndF π β (πΊ β πΉ) β V) |
8 | | f1f 6784 |
. . . . . 6
β’ (πΊ:π΅β1-1βπΆ β πΊ:π΅βΆπΆ) |
9 | | fco 6738 |
. . . . . 6
β’ ((πΊ:π΅βΆπΆ β§ πΉ:πΌβΆπ΅) β (πΊ β πΉ):πΌβΆπΆ) |
10 | 8, 9 | sylan 580 |
. . . . 5
β’ ((πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β (πΊ β πΉ):πΌβΆπΆ) |
11 | 10 | 3adant1 1130 |
. . . 4
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β (πΊ β πΉ):πΌβΆπΆ) |
12 | | dmfex 7894 |
. . . 4
β’ (((πΊ β πΉ) β V β§ (πΊ β πΉ):πΌβΆπΆ) β πΌ β V) |
13 | 7, 11, 12 | syl2anr 597 |
. . 3
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β§ (πΊ β πΉ) LIndF π) β πΌ β V) |
14 | 13 | ex 413 |
. 2
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β ((πΊ β πΉ) LIndF π β πΌ β V)) |
15 | | eldifi 4125 |
. . . . . . . . 9
β’ (π β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β π β (Baseβ(Scalarβπ))) |
16 | | simpllr 774 |
. . . . . . . . . . . . 13
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β πΊ:π΅β1-1βπΆ) |
17 | | lmhmlmod1 20636 |
. . . . . . . . . . . . . . 15
β’ (πΊ β (π LMHom π) β π β LMod) |
18 | 17 | ad3antrrr 728 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β π β LMod) |
19 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β π β (Baseβ(Scalarβπ))) |
20 | | simprl 769 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β πΉ:πΌβΆπ΅) |
21 | | simpl 483 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β πΌ β§ π β (Baseβ(Scalarβπ))) β π₯ β πΌ) |
22 | | ffvelcdm 7080 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:πΌβΆπ΅ β§ π₯ β πΌ) β (πΉβπ₯) β π΅) |
23 | 20, 21, 22 | syl2an 596 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (πΉβπ₯) β π΅) |
24 | | lindfmm.b |
. . . . . . . . . . . . . . 15
β’ π΅ = (Baseβπ) |
25 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(Scalarβπ) =
(Scalarβπ) |
26 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (
Β·π βπ) = ( Β·π
βπ) |
27 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
28 | 24, 25, 26, 27 | lmodvscl 20481 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ (πΉβπ₯) β π΅) β (π( Β·π
βπ)(πΉβπ₯)) β π΅) |
29 | 18, 19, 23, 28 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (π( Β·π
βπ)(πΉβπ₯)) β π΅) |
30 | | imassrn 6068 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (πΌ β {π₯})) β ran πΉ |
31 | | frn 6721 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πΌβΆπ΅ β ran πΉ β π΅) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:πΌβΆπ΅ β§ πΌ β V) β ran πΉ β π΅) |
33 | 30, 32 | sstrid 3992 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:πΌβΆπ΅ β§ πΌ β V) β (πΉ β (πΌ β {π₯})) β π΅) |
34 | 33 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (πΉ β (πΌ β {π₯})) β π΅) |
35 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(LSpanβπ) =
(LSpanβπ) |
36 | 24, 35 | lspssv 20586 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ (πΉ β (πΌ β {π₯})) β π΅) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β π΅) |
37 | 18, 34, 36 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β π΅) |
38 | | f1elima 7258 |
. . . . . . . . . . . . 13
β’ ((πΊ:π΅β1-1βπΆ β§ (π( Β·π
βπ)(πΉβπ₯)) β π΅ β§ ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β π΅) β ((πΊβ(π( Β·π
βπ)(πΉβπ₯))) β (πΊ β ((LSpanβπ)β(πΉ β (πΌ β {π₯})))) β (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))))) |
39 | 16, 29, 37, 38 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β ((πΊβ(π( Β·π
βπ)(πΉβπ₯))) β (πΊ β ((LSpanβπ)β(πΉ β (πΌ β {π₯})))) β (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))))) |
40 | | simplll 773 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β πΊ β (π LMHom π)) |
41 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’ (
Β·π βπ) = ( Β·π
βπ) |
42 | 25, 27, 24, 26, 41 | lmhmlin 20638 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β (π LMHom π) β§ π β (Baseβ(Scalarβπ)) β§ (πΉβπ₯) β π΅) β (πΊβ(π( Β·π
βπ)(πΉβπ₯))) = (π( Β·π
βπ)(πΊβ(πΉβπ₯)))) |
43 | 40, 19, 23, 42 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (πΊβ(π( Β·π
βπ)(πΉβπ₯))) = (π( Β·π
βπ)(πΊβ(πΉβπ₯)))) |
44 | | ffn 6714 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πΌβΆπ΅ β πΉ Fn πΌ) |
45 | 44 | ad2antrl 726 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β πΉ Fn πΌ) |
46 | | fvco2 6985 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ Fn πΌ β§ π₯ β πΌ) β ((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯))) |
47 | 45, 21, 46 | syl2an 596 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β ((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯))) |
48 | 47 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) = (π( Β·π
βπ)(πΊβ(πΉβπ₯)))) |
49 | 43, 48 | eqtr4d 2775 |
. . . . . . . . . . . . 13
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (πΊβ(π( Β·π
βπ)(πΉβπ₯))) = (π( Β·π
βπ)((πΊ β πΉ)βπ₯))) |
50 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’
(LSpanβπ) =
(LSpanβπ) |
51 | 24, 35, 50 | lmhmlsp 20652 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β (π LMHom π) β§ (πΉ β (πΌ β {π₯})) β π΅) β (πΊ β ((LSpanβπ)β(πΉ β (πΌ β {π₯})))) = ((LSpanβπ)β(πΊ β (πΉ β (πΌ β {π₯}))))) |
52 | 40, 34, 51 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (πΊ β ((LSpanβπ)β(πΉ β (πΌ β {π₯})))) = ((LSpanβπ)β(πΊ β (πΉ β (πΌ β {π₯}))))) |
53 | | imaco 6247 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β πΉ) β (πΌ β {π₯})) = (πΊ β (πΉ β (πΌ β {π₯}))) |
54 | 53 | fveq2i 6891 |
. . . . . . . . . . . . . 14
β’
((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))) = ((LSpanβπ)β(πΊ β (πΉ β (πΌ β {π₯})))) |
55 | 52, 54 | eqtr4di 2790 |
. . . . . . . . . . . . 13
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (πΊ β ((LSpanβπ)β(πΉ β (πΌ β {π₯})))) = ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯})))) |
56 | 49, 55 | eleq12d 2827 |
. . . . . . . . . . . 12
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β ((πΊβ(π( Β·π
βπ)(πΉβπ₯))) β (πΊ β ((LSpanβπ)β(πΉ β (πΌ β {π₯})))) β (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
57 | 39, 56 | bitr3d 280 |
. . . . . . . . . . 11
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β ((π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
58 | 57 | notbid 317 |
. . . . . . . . . 10
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ (π₯ β πΌ β§ π β (Baseβ(Scalarβπ)))) β (Β¬ (π(
Β·π βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
59 | 58 | anassrs 468 |
. . . . . . . . 9
β’
(((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ π₯ β πΌ) β§ π β (Baseβ(Scalarβπ))) β (Β¬ (π(
Β·π βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
60 | 15, 59 | sylan2 593 |
. . . . . . . 8
β’
(((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ π₯ β πΌ) β§ π β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) β (Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
61 | 60 | ralbidva 3175 |
. . . . . . 7
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ π₯ β πΌ) β (βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
62 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(Scalarβπ) =
(Scalarβπ) |
63 | 25, 62 | lmhmsca 20633 |
. . . . . . . . . . 11
β’ (πΊ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
64 | 63 | fveq2d 6892 |
. . . . . . . . . 10
β’ (πΊ β (π LMHom π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
65 | 63 | fveq2d 6892 |
. . . . . . . . . . 11
β’ (πΊ β (π LMHom π) β
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ))) |
66 | 65 | sneqd 4639 |
. . . . . . . . . 10
β’ (πΊ β (π LMHom π) β
{(0gβ(Scalarβπ))} =
{(0gβ(Scalarβπ))}) |
67 | 64, 66 | difeq12d 4122 |
. . . . . . . . 9
β’ (πΊ β (π LMHom π) β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) = ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
68 | 67 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ π₯ β πΌ) β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) = ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
69 | 68 | raleqdv 3325 |
. . . . . . 7
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ π₯ β πΌ) β (βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
70 | 61, 69 | bitr4d 281 |
. . . . . 6
β’ ((((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β§ π₯ β πΌ) β (βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
71 | 70 | ralbidva 3175 |
. . . . 5
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β (βπ₯ β πΌ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))) β βπ₯ β πΌ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
72 | 17 | ad2antrr 724 |
. . . . . 6
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β π β LMod) |
73 | | simprr 771 |
. . . . . 6
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β πΌ β V) |
74 | | eqid 2732 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
75 | 24, 26, 35, 25, 27, 74 | islindf2 21360 |
. . . . . 6
β’ ((π β LMod β§ πΌ β V β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β βπ₯ β πΌ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))))) |
76 | 72, 73, 20, 75 | syl3anc 1371 |
. . . . 5
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β (πΉ LIndF π β βπ₯ β πΌ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)(πΉβπ₯)) β ((LSpanβπ)β(πΉ β (πΌ β {π₯}))))) |
77 | | lmhmlmod2 20635 |
. . . . . . 7
β’ (πΊ β (π LMHom π) β π β LMod) |
78 | 77 | ad2antrr 724 |
. . . . . 6
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β π β LMod) |
79 | 10 | ad2ant2lr 746 |
. . . . . 6
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β (πΊ β πΉ):πΌβΆπΆ) |
80 | | lindfmm.c |
. . . . . . 7
β’ πΆ = (Baseβπ) |
81 | | eqid 2732 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
82 | | eqid 2732 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
83 | 80, 41, 50, 62, 81, 82 | islindf2 21360 |
. . . . . 6
β’ ((π β LMod β§ πΌ β V β§ (πΊ β πΉ):πΌβΆπΆ) β ((πΊ β πΉ) LIndF π β βπ₯ β πΌ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
84 | 78, 73, 79, 83 | syl3anc 1371 |
. . . . 5
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β ((πΊ β πΉ) LIndF π β βπ₯ β πΌ βπ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π( Β·π
βπ)((πΊ β πΉ)βπ₯)) β ((LSpanβπ)β((πΊ β πΉ) β (πΌ β {π₯}))))) |
85 | 71, 76, 84 | 3bitr4d 310 |
. . . 4
β’ (((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β§ (πΉ:πΌβΆπ΅ β§ πΌ β V)) β (πΉ LIndF π β (πΊ β πΉ) LIndF π)) |
86 | 85 | exp32 421 |
. . 3
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ) β (πΉ:πΌβΆπ΅ β (πΌ β V β (πΉ LIndF π β (πΊ β πΉ) LIndF π)))) |
87 | 86 | 3impia 1117 |
. 2
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β (πΌ β V β (πΉ LIndF π β (πΊ β πΉ) LIndF π))) |
88 | 6, 14, 87 | pm5.21ndd 380 |
1
β’ ((πΊ β (π LMHom π) β§ πΊ:π΅β1-1βπΆ β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β (πΊ β πΉ) LIndF π)) |