Step | Hyp | Ref
| Expression |
1 | | islssfg.x |
. . 3
β’ π = (π βΎs π) |
2 | | islssfg.s |
. . 3
β’ π = (LSubSpβπ) |
3 | | islssfg.n |
. . 3
β’ π = (LSpanβπ) |
4 | 1, 2, 3 | islssfg 41426 |
. 2
β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β π« π(π β Fin β§ (πβπ) = π))) |
5 | | islssfg2.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
6 | 5, 2 | lssss 20413 |
. . . . . . . . . . . 12
β’ ((πβπ) β π β (πβπ) β π΅) |
7 | 6 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (πβπ) β π) β (πβπ) β π΅) |
8 | | sstr2 3956 |
. . . . . . . . . . 11
β’ (π β (πβπ) β ((πβπ) β π΅ β π β π΅)) |
9 | 7, 8 | mpan9 508 |
. . . . . . . . . 10
β’ (((π β LMod β§ (πβπ) β π) β§ π β (πβπ)) β π β π΅) |
10 | 5, 3 | lspssid 20462 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π΅) β π β (πβπ)) |
11 | 10 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β LMod β§ (πβπ) β π) β§ π β π΅) β π β (πβπ)) |
12 | 9, 11 | impbida 800 |
. . . . . . . . 9
β’ ((π β LMod β§ (πβπ) β π) β (π β (πβπ) β π β π΅)) |
13 | | vex 3452 |
. . . . . . . . . 10
β’ π β V |
14 | 13 | elpw 4569 |
. . . . . . . . 9
β’ (π β π« (πβπ) β π β (πβπ)) |
15 | 13 | elpw 4569 |
. . . . . . . . 9
β’ (π β π« π΅ β π β π΅) |
16 | 12, 14, 15 | 3bitr4g 314 |
. . . . . . . 8
β’ ((π β LMod β§ (πβπ) β π) β (π β π« (πβπ) β π β π« π΅)) |
17 | | eleq1 2826 |
. . . . . . . . . 10
β’ ((πβπ) = π β ((πβπ) β π β π β π)) |
18 | 17 | anbi2d 630 |
. . . . . . . . 9
β’ ((πβπ) = π β ((π β LMod β§ (πβπ) β π) β (π β LMod β§ π β π))) |
19 | | pweq 4579 |
. . . . . . . . . . 11
β’ ((πβπ) = π β π« (πβπ) = π« π) |
20 | 19 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((πβπ) = π β (π β π« (πβπ) β π β π« π)) |
21 | 20 | bibi1d 344 |
. . . . . . . . 9
β’ ((πβπ) = π β ((π β π« (πβπ) β π β π« π΅) β (π β π« π β π β π« π΅))) |
22 | 18, 21 | imbi12d 345 |
. . . . . . . 8
β’ ((πβπ) = π β (((π β LMod β§ (πβπ) β π) β (π β π« (πβπ) β π β π« π΅)) β ((π β LMod β§ π β π) β (π β π« π β π β π« π΅)))) |
23 | 16, 22 | mpbii 232 |
. . . . . . 7
β’ ((πβπ) = π β ((π β LMod β§ π β π) β (π β π« π β π β π« π΅))) |
24 | 23 | com12 32 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ((πβπ) = π β (π β π« π β π β π« π΅))) |
25 | 24 | adantld 492 |
. . . . 5
β’ ((π β LMod β§ π β π) β ((π β Fin β§ (πβπ) = π) β (π β π« π β π β π« π΅))) |
26 | 25 | pm5.32rd 579 |
. . . 4
β’ ((π β LMod β§ π β π) β ((π β π« π β§ (π β Fin β§ (πβπ) = π)) β (π β π« π΅ β§ (π β Fin β§ (πβπ) = π)))) |
27 | | elin 3931 |
. . . . . 6
β’ (π β (π« π΅ β© Fin) β (π β π« π΅ β§ π β Fin)) |
28 | 27 | anbi1i 625 |
. . . . 5
β’ ((π β (π« π΅ β© Fin) β§ (πβπ) = π) β ((π β π« π΅ β§ π β Fin) β§ (πβπ) = π)) |
29 | | anass 470 |
. . . . 5
β’ (((π β π« π΅ β§ π β Fin) β§ (πβπ) = π) β (π β π« π΅ β§ (π β Fin β§ (πβπ) = π))) |
30 | 28, 29 | bitr2i 276 |
. . . 4
β’ ((π β π« π΅ β§ (π β Fin β§ (πβπ) = π)) β (π β (π« π΅ β© Fin) β§ (πβπ) = π)) |
31 | 26, 30 | bitrdi 287 |
. . 3
β’ ((π β LMod β§ π β π) β ((π β π« π β§ (π β Fin β§ (πβπ) = π)) β (π β (π« π΅ β© Fin) β§ (πβπ) = π))) |
32 | 31 | rexbidv2 3172 |
. 2
β’ ((π β LMod β§ π β π) β (βπ β π« π(π β Fin β§ (πβπ) = π) β βπ β (π« π΅ β© Fin)(πβπ) = π)) |
33 | 4, 32 | bitrd 279 |
1
β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β (π« π΅ β© Fin)(πβπ) = π)) |