Step | Hyp | Ref
| Expression |
1 | | lsmfgcl.f |
. 2
β’ πΉ = (π βΎs (π΄ β π΅)) |
2 | | lsmfgcl.df |
. . . 4
β’ (π β π· β LFinGen) |
3 | | lsmfgcl.w |
. . . . 5
β’ (π β π β LMod) |
4 | | lsmfgcl.a |
. . . . 5
β’ (π β π΄ β π) |
5 | | lsmfgcl.d |
. . . . . 6
β’ π· = (π βΎs π΄) |
6 | | lsmfgcl.u |
. . . . . 6
β’ π = (LSubSpβπ) |
7 | | eqid 2737 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
8 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
9 | 5, 6, 7, 8 | islssfg2 41427 |
. . . . 5
β’ ((π β LMod β§ π΄ β π) β (π· β LFinGen β βπ β (π«
(Baseβπ) β©
Fin)((LSpanβπ)βπ) = π΄)) |
10 | 3, 4, 9 | syl2anc 585 |
. . . 4
β’ (π β (π· β LFinGen β βπ β (π«
(Baseβπ) β©
Fin)((LSpanβπ)βπ) = π΄)) |
11 | 2, 10 | mpbid 231 |
. . 3
β’ (π β βπ β (π« (Baseβπ) β© Fin)((LSpanβπ)βπ) = π΄) |
12 | | lsmfgcl.ef |
. . . . . . . 8
β’ (π β πΈ β LFinGen) |
13 | | lsmfgcl.b |
. . . . . . . . 9
β’ (π β π΅ β π) |
14 | | lsmfgcl.e |
. . . . . . . . . 10
β’ πΈ = (π βΎs π΅) |
15 | 14, 6, 7, 8 | islssfg2 41427 |
. . . . . . . . 9
β’ ((π β LMod β§ π΅ β π) β (πΈ β LFinGen β βπ β (π«
(Baseβπ) β©
Fin)((LSpanβπ)βπ) = π΅)) |
16 | 3, 13, 15 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΈ β LFinGen β βπ β (π«
(Baseβπ) β©
Fin)((LSpanβπ)βπ) = π΅)) |
17 | 12, 16 | mpbid 231 |
. . . . . . 7
β’ (π β βπ β (π« (Baseβπ) β© Fin)((LSpanβπ)βπ) = π΅) |
18 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (π« (Baseβπ) β© Fin)) β
βπ β (π«
(Baseβπ) β©
Fin)((LSpanβπ)βπ) = π΅) |
19 | | inss1 4193 |
. . . . . . . . . . . . . . 15
β’
(π« (Baseβπ) β© Fin) β π«
(Baseβπ) |
20 | 19 | sseli 3945 |
. . . . . . . . . . . . . 14
β’ (π β (π«
(Baseβπ) β© Fin)
β π β π«
(Baseβπ)) |
21 | 20 | elpwid 4574 |
. . . . . . . . . . . . 13
β’ (π β (π«
(Baseβπ) β© Fin)
β π β
(Baseβπ)) |
22 | 19 | sseli 3945 |
. . . . . . . . . . . . . 14
β’ (π β (π«
(Baseβπ) β© Fin)
β π β π«
(Baseβπ)) |
23 | 22 | elpwid 4574 |
. . . . . . . . . . . . 13
β’ (π β (π«
(Baseβπ) β© Fin)
β π β
(Baseβπ)) |
24 | | lsmfgcl.p |
. . . . . . . . . . . . . 14
β’ β =
(LSSumβπ) |
25 | 8, 7, 24 | lsmsp2 20564 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β (Baseβπ) β§ π β (Baseβπ)) β (((LSpanβπ)βπ) β ((LSpanβπ)βπ)) = ((LSpanβπ)β(π βͺ π))) |
26 | 3, 21, 23, 25 | syl3an 1161 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin))
β (((LSpanβπ)βπ) β ((LSpanβπ)βπ)) = ((LSpanβπ)β(π βͺ π))) |
27 | 26 | 3expb 1121 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β (((LSpanβπ)βπ) β ((LSpanβπ)βπ)) = ((LSpanβπ)β(π βͺ π))) |
28 | 27 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β (π
βΎs (((LSpanβπ)βπ) β ((LSpanβπ)βπ))) = (π βΎs ((LSpanβπ)β(π βͺ π)))) |
29 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β π β
LMod) |
30 | | unss 4149 |
. . . . . . . . . . . . . 14
β’ ((π β (Baseβπ) β§ π β (Baseβπ)) β (π βͺ π) β (Baseβπ)) |
31 | 30 | biimpi 215 |
. . . . . . . . . . . . 13
β’ ((π β (Baseβπ) β§ π β (Baseβπ)) β (π βͺ π) β (Baseβπ)) |
32 | 21, 23, 31 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β (π«
(Baseβπ) β© Fin)
β§ π β (π«
(Baseβπ) β© Fin))
β (π βͺ π) β (Baseβπ)) |
33 | 32 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β (π βͺ π) β (Baseβπ)) |
34 | | inss2 4194 |
. . . . . . . . . . . . . 14
β’
(π« (Baseβπ) β© Fin) β Fin |
35 | 34 | sseli 3945 |
. . . . . . . . . . . . 13
β’ (π β (π«
(Baseβπ) β© Fin)
β π β
Fin) |
36 | 34 | sseli 3945 |
. . . . . . . . . . . . 13
β’ (π β (π«
(Baseβπ) β© Fin)
β π β
Fin) |
37 | | unfi 9123 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π β Fin) β (π βͺ π) β Fin) |
38 | 35, 36, 37 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β (π«
(Baseβπ) β© Fin)
β§ π β (π«
(Baseβπ) β© Fin))
β (π βͺ π) β Fin) |
39 | 38 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β (π βͺ π) β Fin) |
40 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π βΎs
((LSpanβπ)β(π βͺ π))) = (π βΎs ((LSpanβπ)β(π βͺ π))) |
41 | 7, 8, 40 | islssfgi 41428 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (π βͺ π) β (Baseβπ) β§ (π βͺ π) β Fin) β (π βΎs ((LSpanβπ)β(π βͺ π))) β LFinGen) |
42 | 29, 33, 39, 41 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β (π
βΎs ((LSpanβπ)β(π βͺ π))) β LFinGen) |
43 | 28, 42 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ (π β (π« (Baseβπ) β© Fin) β§ π β (π«
(Baseβπ) β© Fin)))
β (π
βΎs (((LSpanβπ)βπ) β ((LSpanβπ)βπ))) β LFinGen) |
44 | 43 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β (π« (Baseβπ) β© Fin)) β§ π β (π«
(Baseβπ) β© Fin))
β (π
βΎs (((LSpanβπ)βπ) β ((LSpanβπ)βπ))) β LFinGen) |
45 | | oveq2 7370 |
. . . . . . . . . 10
β’
(((LSpanβπ)βπ) = π΅ β (((LSpanβπ)βπ) β ((LSpanβπ)βπ)) = (((LSpanβπ)βπ) β π΅)) |
46 | 45 | oveq2d 7378 |
. . . . . . . . 9
β’
(((LSpanβπ)βπ) = π΅ β (π βΎs (((LSpanβπ)βπ) β ((LSpanβπ)βπ))) = (π βΎs (((LSpanβπ)βπ) β π΅))) |
47 | 46 | eleq1d 2823 |
. . . . . . . 8
β’
(((LSpanβπ)βπ) = π΅ β ((π βΎs (((LSpanβπ)βπ) β ((LSpanβπ)βπ))) β LFinGen β (π βΎs (((LSpanβπ)βπ) β π΅)) β LFinGen)) |
48 | 44, 47 | syl5ibcom 244 |
. . . . . . 7
β’ (((π β§ π β (π« (Baseβπ) β© Fin)) β§ π β (π«
(Baseβπ) β© Fin))
β (((LSpanβπ)βπ) = π΅ β (π βΎs (((LSpanβπ)βπ) β π΅)) β LFinGen)) |
49 | 48 | rexlimdva 3153 |
. . . . . 6
β’ ((π β§ π β (π« (Baseβπ) β© Fin)) β
(βπ β (π«
(Baseβπ) β©
Fin)((LSpanβπ)βπ) = π΅ β (π βΎs (((LSpanβπ)βπ) β π΅)) β LFinGen)) |
50 | 18, 49 | mpd 15 |
. . . . 5
β’ ((π β§ π β (π« (Baseβπ) β© Fin)) β (π βΎs
(((LSpanβπ)βπ) β π΅)) β LFinGen) |
51 | | oveq1 7369 |
. . . . . . 7
β’
(((LSpanβπ)βπ) = π΄ β (((LSpanβπ)βπ) β π΅) = (π΄ β π΅)) |
52 | 51 | oveq2d 7378 |
. . . . . 6
β’
(((LSpanβπ)βπ) = π΄ β (π βΎs (((LSpanβπ)βπ) β π΅)) = (π βΎs (π΄ β π΅))) |
53 | 52 | eleq1d 2823 |
. . . . 5
β’
(((LSpanβπ)βπ) = π΄ β ((π βΎs (((LSpanβπ)βπ) β π΅)) β LFinGen β (π βΎs (π΄ β π΅)) β LFinGen)) |
54 | 50, 53 | syl5ibcom 244 |
. . . 4
β’ ((π β§ π β (π« (Baseβπ) β© Fin)) β
(((LSpanβπ)βπ) = π΄ β (π βΎs (π΄ β π΅)) β LFinGen)) |
55 | 54 | rexlimdva 3153 |
. . 3
β’ (π β (βπ β (π« (Baseβπ) β© Fin)((LSpanβπ)βπ) = π΄ β (π βΎs (π΄ β π΅)) β LFinGen)) |
56 | 11, 55 | mpd 15 |
. 2
β’ (π β (π βΎs (π΄ β π΅)) β LFinGen) |
57 | 1, 56 | eqeltrid 2842 |
1
β’ (π β πΉ β LFinGen) |