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 37470 |
. . 3
β’ (π β LMod β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
7 | 1, 6 | syl 17 |
. 2
β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
8 | 1 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β π β LMod) |
9 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β π β π) |
10 | 4, 3 | lspid 20459 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π) β (πβπ) = π) |
11 | 8, 9, 10 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβπ) = π) |
12 | 11 | uneq1d 4127 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β ((πβπ) βͺ (πβ{π£})) = (π βͺ (πβ{π£}))) |
13 | 12 | fveq2d 6851 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβ((πβπ) βͺ (πβ{π£}))) = (πβ(π βͺ (πβ{π£})))) |
14 | 2, 4 | lssss 20413 |
. . . . . . . . . 10
β’ (π β π β π β π) |
15 | 9, 14 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β π β π) |
16 | | snssi 4773 |
. . . . . . . . . 10
β’ (π£ β π β {π£} β π) |
17 | 16 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β {π£} β π) |
18 | 2, 3 | lspun 20464 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ {π£} β π) β (πβ(π βͺ {π£})) = (πβ((πβπ) βͺ (πβ{π£})))) |
19 | 8, 15, 17, 18 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβ(π βͺ {π£})) = (πβ((πβπ) βͺ (πβ{π£})))) |
20 | 2, 4, 3 | lspcl 20453 |
. . . . . . . . . 10
β’ ((π β LMod β§ {π£} β π) β (πβ{π£}) β π) |
21 | 8, 17, 20 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (πβ{π£}) β π) |
22 | | islshpsm.p |
. . . . . . . . . 10
β’ β =
(LSSumβπ) |
23 | 4, 3, 22 | lsmsp 20563 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ (πβ{π£}) β π) β (π β (πβ{π£})) = (πβ(π βͺ (πβ{π£})))) |
24 | 8, 9, 21, 23 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (π β (πβ{π£})) = (πβ(π βͺ (πβ{π£})))) |
25 | 13, 19, 24 | 3eqtr4rd 2788 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β (π β (πβ{π£})) = (πβ(π βͺ {π£}))) |
26 | 25 | eqeq1d 2739 |
. . . . . 6
β’ (((π β§ (π β π β§ π β π)) β§ π£ β π) β ((π β (πβ{π£})) = π β (πβ(π βͺ {π£})) = π)) |
27 | 26 | rexbidva 3174 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (βπ£ β π (π β (πβ{π£})) = π β βπ£ β π (πβ(π βͺ {π£})) = π)) |
28 | 27 | pm5.32da 580 |
. . . 4
β’ (π β (((π β π β§ π β π) β§ βπ£ β π (π β (πβ{π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
29 | 28 | bicomd 222 |
. . 3
β’ (π β (((π β π β§ π β π) β§ βπ£ β π (πβ(π βͺ {π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (π β (πβ{π£})) = π))) |
30 | | df-3an 1090 |
. . 3
β’ ((π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (πβ(π βͺ {π£})) = π)) |
31 | | df-3an 1090 |
. . 3
β’ ((π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (π β (πβ{π£})) = π)) |
32 | 29, 30, 31 | 3bitr4g 314 |
. 2
β’ (π β ((π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π) β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) |
33 | 7, 32 | bitrd 279 |
1
β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) |