Step | Hyp | Ref
| Expression |
1 | | islinds3.b |
. . . . 5
β’ π΅ = (Baseβπ) |
2 | 1 | linds1 21232 |
. . . 4
β’ (π β (LIndSβπ) β π β π΅) |
3 | 2 | a1i 11 |
. . 3
β’ (π β LMod β (π β (LIndSβπ) β π β π΅)) |
4 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
5 | 4 | linds1 21232 |
. . . . . 6
β’ (π β (LIndSβπ) β π β (Baseβπ)) |
6 | | islinds3.x |
. . . . . . 7
β’ π = (π βΎs (πΎβπ)) |
7 | 6, 1 | ressbasss 17126 |
. . . . . 6
β’
(Baseβπ)
β π΅ |
8 | 5, 7 | sstrdi 3957 |
. . . . 5
β’ (π β (LIndSβπ) β π β π΅) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)) β π β π΅) |
10 | 9 | a1i 11 |
. . 3
β’ (π β LMod β ((π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)) β π β π΅)) |
11 | | simpl 484 |
. . . . . . . 8
β’ ((π β LMod β§ π β π΅) β π β LMod) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(LSubSpβπ) =
(LSubSpβπ) |
13 | | islinds3.k |
. . . . . . . . 9
β’ πΎ = (LSpanβπ) |
14 | 1, 12, 13 | lspcl 20452 |
. . . . . . . 8
β’ ((π β LMod β§ π β π΅) β (πΎβπ) β (LSubSpβπ)) |
15 | 1, 13 | lspssid 20461 |
. . . . . . . 8
β’ ((π β LMod β§ π β π΅) β π β (πΎβπ)) |
16 | | eqid 2733 |
. . . . . . . . 9
β’
(LSpanβπ) =
(LSpanβπ) |
17 | 6, 13, 16, 12 | lsslsp 20491 |
. . . . . . . 8
β’ ((π β LMod β§ (πΎβπ) β (LSubSpβπ) β§ π β (πΎβπ)) β (πΎβπ) = ((LSpanβπ)βπ)) |
18 | 11, 14, 15, 17 | syl3anc 1372 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β (πΎβπ) = ((LSpanβπ)βπ)) |
19 | 1, 13 | lspssv 20459 |
. . . . . . . 8
β’ ((π β LMod β§ π β π΅) β (πΎβπ) β π΅) |
20 | 6, 1 | ressbas2 17125 |
. . . . . . . 8
β’ ((πΎβπ) β π΅ β (πΎβπ) = (Baseβπ)) |
21 | 19, 20 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β (πΎβπ) = (Baseβπ)) |
22 | 18, 21 | eqtr3d 2775 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β ((LSpanβπ)βπ) = (Baseβπ)) |
23 | 22 | biantrud 533 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β (π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)))) |
24 | 12, 6 | lsslinds 21253 |
. . . . . . . 8
β’ ((π β LMod β§ (πΎβπ) β (LSubSpβπ) β§ π β (πΎβπ)) β (π β (LIndSβπ) β π β (LIndSβπ))) |
25 | 11, 14, 15, 24 | syl3anc 1372 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β π β (LIndSβπ))) |
26 | 25 | bicomd 222 |
. . . . . 6
β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β π β (LIndSβπ))) |
27 | 26 | anbi1d 631 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β ((π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)) β (π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)))) |
28 | 23, 27 | bitrd 279 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β (π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)))) |
29 | 28 | ex 414 |
. . 3
β’ (π β LMod β (π β π΅ β (π β (LIndSβπ) β (π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ))))) |
30 | 3, 10, 29 | pm5.21ndd 381 |
. 2
β’ (π β LMod β (π β (LIndSβπ) β (π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ)))) |
31 | | islinds3.j |
. . 3
β’ π½ = (LBasisβπ) |
32 | 4, 31, 16 | islbs4 21254 |
. 2
β’ (π β π½ β (π β (LIndSβπ) β§ ((LSpanβπ)βπ) = (Baseβπ))) |
33 | 30, 32 | bitr4di 289 |
1
β’ (π β LMod β (π β (LIndSβπ) β π β π½)) |