Step | Hyp | Ref
| Expression |
1 | | simp3 1138 |
. . 3
β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β πΌ β π΅) |
2 | | bren 8951 |
. . 3
β’ (πΌ β π΅ β βπ π:πΌβ1-1-ontoβπ΅) |
3 | 1, 2 | sylib 217 |
. 2
β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β βπ π:πΌβ1-1-ontoβπ΅) |
4 | | eqid 2732 |
. . . 4
β’ (πΉ freeLMod πΌ) = (πΉ freeLMod πΌ) |
5 | | eqid 2732 |
. . . 4
β’
(Baseβ(πΉ
freeLMod πΌ)) =
(Baseβ(πΉ freeLMod
πΌ)) |
6 | | eqid 2732 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
7 | | eqid 2732 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
8 | | eqid 2732 |
. . . 4
β’
(LSpanβπ) =
(LSpanβπ) |
9 | | eqid 2732 |
. . . 4
β’ (π₯ β (Baseβ(πΉ freeLMod πΌ)) β¦ (π Ξ£g (π₯ βf (
Β·π βπ)π))) = (π₯ β (Baseβ(πΉ freeLMod πΌ)) β¦ (π Ξ£g (π₯ βf (
Β·π βπ)π))) |
10 | | simpl1 1191 |
. . . 4
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β π β LMod) |
11 | | relen 8946 |
. . . . . . 7
β’ Rel
β |
12 | 11 | brrelex1i 5732 |
. . . . . 6
β’ (πΌ β π΅ β πΌ β V) |
13 | 12 | 3ad2ant3 1135 |
. . . . 5
β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β πΌ β V) |
14 | 13 | adantr 481 |
. . . 4
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β πΌ β V) |
15 | | lbslcic.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
16 | 15 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β πΉ = (Scalarβπ)) |
17 | | f1ofo 6840 |
. . . . 5
β’ (π:πΌβ1-1-ontoβπ΅ β π:πΌβontoβπ΅) |
18 | 17 | adantl 482 |
. . . 4
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β π:πΌβontoβπ΅) |
19 | | lbslcic.j |
. . . . . . . . 9
β’ π½ = (LBasisβπ) |
20 | 19 | lbslinds 21607 |
. . . . . . . 8
β’ π½ β (LIndSβπ) |
21 | 20 | sseli 3978 |
. . . . . . 7
β’ (π΅ β π½ β π΅ β (LIndSβπ)) |
22 | 21 | 3ad2ant2 1134 |
. . . . . 6
β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β π΅ β (LIndSβπ)) |
23 | 22 | adantr 481 |
. . . . 5
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β π΅ β (LIndSβπ)) |
24 | | f1of1 6832 |
. . . . . 6
β’ (π:πΌβ1-1-ontoβπ΅ β π:πΌβ1-1βπ΅) |
25 | 24 | adantl 482 |
. . . . 5
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β π:πΌβ1-1βπ΅) |
26 | | f1linds 21599 |
. . . . 5
β’ ((π β LMod β§ π΅ β (LIndSβπ) β§ π:πΌβ1-1βπ΅) β π LIndF π) |
27 | 10, 23, 25, 26 | syl3anc 1371 |
. . . 4
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β π LIndF π) |
28 | 6, 19, 8 | lbssp 20834 |
. . . . . 6
β’ (π΅ β π½ β ((LSpanβπ)βπ΅) = (Baseβπ)) |
29 | 28 | 3ad2ant2 1134 |
. . . . 5
β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β ((LSpanβπ)βπ΅) = (Baseβπ)) |
30 | 29 | adantr 481 |
. . . 4
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β ((LSpanβπ)βπ΅) = (Baseβπ)) |
31 | 4, 5, 6, 7, 8, 9, 10, 14, 16, 18, 27, 30 | indlcim 21614 |
. . 3
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β (π₯ β (Baseβ(πΉ freeLMod πΌ)) β¦ (π Ξ£g (π₯ βf (
Β·π βπ)π))) β ((πΉ freeLMod πΌ) LMIso π)) |
32 | | lmimcnv 20822 |
. . 3
β’ ((π₯ β (Baseβ(πΉ freeLMod πΌ)) β¦ (π Ξ£g (π₯ βf (
Β·π βπ)π))) β ((πΉ freeLMod πΌ) LMIso π) β β‘(π₯ β (Baseβ(πΉ freeLMod πΌ)) β¦ (π Ξ£g (π₯ βf (
Β·π βπ)π))) β (π LMIso (πΉ freeLMod πΌ))) |
33 | | brlmici 20824 |
. . 3
β’ (β‘(π₯ β (Baseβ(πΉ freeLMod πΌ)) β¦ (π Ξ£g (π₯ βf (
Β·π βπ)π))) β (π LMIso (πΉ freeLMod πΌ)) β π βπ (πΉ freeLMod πΌ)) |
34 | 31, 32, 33 | 3syl 18 |
. 2
β’ (((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β§ π:πΌβ1-1-ontoβπ΅) β π βπ (πΉ freeLMod πΌ)) |
35 | 3, 34 | exlimddv 1938 |
1
β’ ((π β LMod β§ π΅ β π½ β§ πΌ β π΅) β π βπ (πΉ freeLMod πΌ)) |