Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’ (π freeLMod π) = (π freeLMod π) |
2 | | eqid 2737 |
. . . 4
β’
(Baseβ(π
freeLMod π)) =
(Baseβ(π freeLMod
π)) |
3 | | eqid 2737 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
4 | | eqid 2737 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
5 | | eqid 2737 |
. . . 4
β’ (π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) = (π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) |
6 | | fglmod 41429 |
. . . . 5
β’ (π β LFinGen β π β LMod) |
7 | 6 | ad3antrrr 729 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β π β LMod) |
8 | | vex 3452 |
. . . . 5
β’ π β V |
9 | 8 | a1i 11 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β π β V) |
10 | | lnrfg.s |
. . . . 5
β’ π = (Scalarβπ) |
11 | 10 | a1i 11 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β π = (Scalarβπ)) |
12 | | f1oi 6827 |
. . . . . . 7
β’ ( I
βΎ π):πβ1-1-ontoβπ |
13 | | f1of 6789 |
. . . . . . 7
β’ (( I
βΎ π):πβ1-1-ontoβπ β ( I βΎ π):πβΆπ) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
β’ ( I
βΎ π):πβΆπ |
15 | | elpwi 4572 |
. . . . . 6
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
16 | | fss 6690 |
. . . . . 6
β’ ((( I
βΎ π):πβΆπ β§ π β (Baseβπ)) β ( I βΎ π):πβΆ(Baseβπ)) |
17 | 14, 15, 16 | sylancr 588 |
. . . . 5
β’ (π β π«
(Baseβπ) β ( I
βΎ π):πβΆ(Baseβπ)) |
18 | 17 | ad2antlr 726 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β ( I βΎ π):πβΆ(Baseβπ)) |
19 | 1, 2, 3, 4, 5, 7, 9, 11, 18 | frlmup1 21220 |
. . 3
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β (π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) β ((π freeLMod π) LMHom π)) |
20 | | simpllr 775 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β π β LNoeR) |
21 | | simprl 770 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β π β Fin) |
22 | 1 | lnrfrlm 41474 |
. . . 4
β’ ((π β LNoeR β§ π β Fin) β (π freeLMod π) β LNoeM) |
23 | 20, 21, 22 | syl2anc 585 |
. . 3
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β (π freeLMod π) β LNoeM) |
24 | | eqid 2737 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
25 | 1, 2, 3, 4, 5, 7, 9, 11, 18, 24 | frlmup3 21222 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β ran (π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) = ((LSpanβπ)βran ( I βΎ π))) |
26 | | rnresi 6032 |
. . . . . 6
β’ ran ( I
βΎ π) = π |
27 | 26 | fveq2i 6850 |
. . . . 5
β’
((LSpanβπ)βran ( I βΎ π)) = ((LSpanβπ)βπ) |
28 | | simprr 772 |
. . . . 5
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β ((LSpanβπ)βπ) = (Baseβπ)) |
29 | 27, 28 | eqtrid 2789 |
. . . 4
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β ((LSpanβπ)βran ( I βΎ π)) = (Baseβπ)) |
30 | 25, 29 | eqtrd 2777 |
. . 3
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β ran (π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) = (Baseβπ)) |
31 | 3 | lnmepi 41441 |
. . 3
β’ (((π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) β ((π freeLMod π) LMHom π) β§ (π freeLMod π) β LNoeM β§ ran (π β (Baseβ(π freeLMod π)) β¦ (π Ξ£g (π βf (
Β·π βπ)( I βΎ π)))) = (Baseβπ)) β π β LNoeM) |
32 | 19, 23, 30, 31 | syl3anc 1372 |
. 2
β’ ((((π β LFinGen β§ π β LNoeR) β§ π β π«
(Baseβπ)) β§
(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) β π β LNoeM) |
33 | 3, 24 | islmodfg 41425 |
. . . . 5
β’ (π β LMod β (π β LFinGen β
βπ β π«
(Baseβπ)(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ)))) |
34 | 6, 33 | syl 17 |
. . . 4
β’ (π β LFinGen β (π β LFinGen β
βπ β π«
(Baseβπ)(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ)))) |
35 | 34 | ibi 267 |
. . 3
β’ (π β LFinGen β
βπ β π«
(Baseβπ)(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) |
36 | 35 | adantr 482 |
. 2
β’ ((π β LFinGen β§ π β LNoeR) β
βπ β π«
(Baseβπ)(π β Fin β§
((LSpanβπ)βπ) = (Baseβπ))) |
37 | 32, 36 | r19.29a 3160 |
1
β’ ((π β LFinGen β§ π β LNoeR) β π β LNoeM) |