Step | Hyp | Ref
| Expression |
1 | | df-lfig 41424 |
. . . 4
β’ LFinGen =
{π β LMod β£
(Baseβπ) β
((LSpanβπ) β
(π« (Baseβπ)
β© Fin))} |
2 | 1 | eleq2i 2830 |
. . 3
β’ (π β LFinGen β π β {π β LMod β£ (Baseβπ) β ((LSpanβπ) β (π«
(Baseβπ) β©
Fin))}) |
3 | | fveq2 6847 |
. . . . 5
β’ (π = π β (Baseβπ) = (Baseβπ)) |
4 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (LSpanβπ) = (LSpanβπ)) |
5 | | islmodfg.n |
. . . . . . 7
β’ π = (LSpanβπ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . 6
β’ (π = π β (LSpanβπ) = π) |
7 | 3 | pweqd 4582 |
. . . . . . 7
β’ (π = π β π« (Baseβπ) = π« (Baseβπ)) |
8 | 7 | ineq1d 4176 |
. . . . . 6
β’ (π = π β (π« (Baseβπ) β© Fin) = (π«
(Baseβπ) β©
Fin)) |
9 | 6, 8 | imaeq12d 6019 |
. . . . 5
β’ (π = π β ((LSpanβπ) β (π« (Baseβπ) β© Fin)) = (π β (π«
(Baseβπ) β©
Fin))) |
10 | 3, 9 | eleq12d 2832 |
. . . 4
β’ (π = π β ((Baseβπ) β ((LSpanβπ) β (π« (Baseβπ) β© Fin)) β
(Baseβπ) β
(π β (π«
(Baseβπ) β©
Fin)))) |
11 | 10 | elrab3 3651 |
. . 3
β’ (π β LMod β (π β {π β LMod β£ (Baseβπ) β ((LSpanβπ) β (π«
(Baseβπ) β© Fin))}
β (Baseβπ)
β (π β
(π« (Baseβπ)
β© Fin)))) |
12 | 2, 11 | bitrid 283 |
. 2
β’ (π β LMod β (π β LFinGen β
(Baseβπ) β
(π β (π«
(Baseβπ) β©
Fin)))) |
13 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
14 | | eqid 2737 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
15 | 13, 14, 5 | lspf 20451 |
. . . . 5
β’ (π β LMod β π:π« (Baseβπ)βΆ(LSubSpβπ)) |
16 | 15 | ffnd 6674 |
. . . 4
β’ (π β LMod β π Fn π« (Baseβπ)) |
17 | | inss1 4193 |
. . . 4
β’
(π« (Baseβπ) β© Fin) β π«
(Baseβπ) |
18 | | fvelimab 6919 |
. . . 4
β’ ((π Fn π« (Baseβπ) β§ (π«
(Baseβπ) β© Fin)
β π« (Baseβπ)) β ((Baseβπ) β (π β (π« (Baseβπ) β© Fin)) β
βπ β (π«
(Baseβπ) β©
Fin)(πβπ) = (Baseβπ))) |
19 | 16, 17, 18 | sylancl 587 |
. . 3
β’ (π β LMod β
((Baseβπ) β
(π β (π«
(Baseβπ) β© Fin))
β βπ β
(π« (Baseβπ)
β© Fin)(πβπ) = (Baseβπ))) |
20 | | elin 3931 |
. . . . . . 7
β’ (π β (π«
(Baseβπ) β© Fin)
β (π β π«
(Baseβπ) β§ π β Fin)) |
21 | | islmodfg.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ) |
22 | 21 | eqcomi 2746 |
. . . . . . . . . 10
β’
(Baseβπ) =
π΅ |
23 | 22 | pweqi 4581 |
. . . . . . . . 9
β’ π«
(Baseβπ) = π«
π΅ |
24 | 23 | eleq2i 2830 |
. . . . . . . 8
β’ (π β π«
(Baseβπ) β π β π« π΅) |
25 | 24 | anbi1i 625 |
. . . . . . 7
β’ ((π β π«
(Baseβπ) β§ π β Fin) β (π β π« π΅ β§ π β Fin)) |
26 | 20, 25 | bitri 275 |
. . . . . 6
β’ (π β (π«
(Baseβπ) β© Fin)
β (π β π«
π΅ β§ π β Fin)) |
27 | 22 | eqeq2i 2750 |
. . . . . 6
β’ ((πβπ) = (Baseβπ) β (πβπ) = π΅) |
28 | 26, 27 | anbi12i 628 |
. . . . 5
β’ ((π β (π«
(Baseβπ) β© Fin)
β§ (πβπ) = (Baseβπ)) β ((π β π« π΅ β§ π β Fin) β§ (πβπ) = π΅)) |
29 | | anass 470 |
. . . . 5
β’ (((π β π« π΅ β§ π β Fin) β§ (πβπ) = π΅) β (π β π« π΅ β§ (π β Fin β§ (πβπ) = π΅))) |
30 | 28, 29 | bitri 275 |
. . . 4
β’ ((π β (π«
(Baseβπ) β© Fin)
β§ (πβπ) = (Baseβπ)) β (π β π« π΅ β§ (π β Fin β§ (πβπ) = π΅))) |
31 | 30 | rexbii2 3094 |
. . 3
β’
(βπ β
(π« (Baseβπ)
β© Fin)(πβπ) = (Baseβπ) β βπ β π« π΅(π β Fin β§ (πβπ) = π΅)) |
32 | 19, 31 | bitrdi 287 |
. 2
β’ (π β LMod β
((Baseβπ) β
(π β (π«
(Baseβπ) β© Fin))
β βπ β
π« π΅(π β Fin β§ (πβπ) = π΅))) |
33 | 12, 32 | bitrd 279 |
1
β’ (π β LMod β (π β LFinGen β
βπ β π«
π΅(π β Fin β§ (πβπ) = π΅))) |