| Step | Hyp | Ref
| Expression |
|---|
| 1 | | islshpsm.w |
. . 3
β’ (π β π β LMod) |
| 2 | | islshpsm.v |
. . . 4
β’ π = (Baseβπ) |
| 3 | | islshpsm.n |
. . . 4
β’ π = (LSpanβπ) |
| 4 | | islshpsm.s |
. . . 4
β’ π = (LSubSpβπ) |
| 5 | | islshpsm.h |
. . . 4
β’ π» = (LSHypβπ) |
| 6 | 2, 3, 4, 5 | islshp 37837 |
. . 3
β’ (π β LMod β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
| 7 | 1, 6 | syl 17 |
. 2
β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
| 8 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β π β LMod) |
| 9 | | simplrl 775 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β π β π) |
| 10 | 4, 3 | lspid 20585 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π) β (πβπ) = π) |
| 11 | 8, 9, 10 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβπ) = π) |
| 12 | 11 | uneq1d 4161 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β ((πβπ) βͺ (πβ{π£})) = (π βͺ (πβ{π£}))) |
| 13 | 12 | fveq2d 6892 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβ((πβπ) βͺ (πβ{π£}))) = (πβ(π βͺ (πβ{π£})))) |
| 14 | 2, 4 | lssss 20539 |
. . . . . . . . . 10
β’ (π β π β π β π) |
| 15 | 9, 14 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β π β π) |
| 16 | | snssi 4810 |
. . . . . . . . . 10
β’ (π£ β π β {π£} β π) |
| 17 | 16 | adantl 482 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β {π£} β π) |
| 18 | 2, 3 | lspun 20590 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ {π£} β π) β (πβ(π βͺ {π£})) = (πβ((πβπ) βͺ (πβ{π£})))) |
| 19 | 8, 15, 17, 18 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβ(π βͺ {π£})) = (πβ((πβπ) βͺ (πβ{π£})))) |
| 20 | 2, 4, 3 | lspcl 20579 |
. . . . . . . . . 10
β’ ((π β LMod β§ {π£} β π) β (πβ{π£}) β π) |
| 21 | 8, 17, 20 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβ{π£}) β π) |
| 22 | | islshpsm.p |
. . . . . . . . . 10
β’ β =
(LSSumβπ) |
| 23 | 4, 3, 22 | lsmsp 20689 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ (πβ{π£}) β π) β (π β (πβ{π£})) = (πβ(π βͺ (πβ{π£})))) |
| 24 | 8, 9, 21, 23 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (π β (πβ{π£})) = (πβ(π βͺ (πβ{π£})))) |
| 25 | 13, 19, 24 | 3eqtr4rd 2783 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (π β (πβ{π£})) = (πβ(π βͺ {π£}))) |
| 26 | 25 | eqeq1d 2734 |
. . . . . 6
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β ((π β (πβ{π£})) = π β (πβ(π βͺ {π£})) = π)) |
| 27 | 26 | rexbidva 3176 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (βπ£ β π (π β (πβ{π£})) = π β βπ£ β π (πβ(π βͺ {π£})) = π)) |
| 28 | 27 | pm5.32da 579 |
. . . 4
β’ (π β (((π β π β§ π β π) β§ βπ£ β π (π β (πβ{π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
| 29 | 28 | bicomd 222 |
. . 3
β’ (π β (((π β π β§ π β π) β§ βπ£ β π (πβ(π βͺ {π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (π β (πβ{π£})) = π))) |
| 30 | | df-3an 1089 |
. . 3
β’ ((π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (πβ(π βͺ {π£})) = π)) |
| 31 | | df-3an 1089 |
. . 3
β’ ((π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (π β (πβ{π£})) = π)) |
| 32 | 29, 30, 31 | 3bitr4g 313 |
. 2
β’ (π β ((π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π) β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) |
| 33 | 7, 32 | bitrd 278 |
1
β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) |
