Step | Hyp | Ref
| Expression |
1 | | lshpnel2.e |
. . . 4
β’ (π β Β¬ π β π) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ π β π») β Β¬ π β π) |
3 | | lshpnel2.v |
. . . 4
β’ π = (Baseβπ) |
4 | | lshpnel2.n |
. . . 4
β’ π = (LSpanβπ) |
5 | | lshpnel2.p |
. . . 4
β’ β =
(LSSumβπ) |
6 | | lshpnel2.h |
. . . 4
β’ π» = (LSHypβπ) |
7 | | lshpnel2.w |
. . . . 5
β’ (π β π β LVec) |
8 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π β π») β π β LVec) |
9 | | simpr 486 |
. . . 4
β’ ((π β§ π β π») β π β π») |
10 | | lshpnel2.x |
. . . . 5
β’ (π β π β π) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ π β π») β π β π) |
12 | 3, 4, 5, 6, 8, 9, 11 | lshpnelb 37475 |
. . 3
β’ ((π β§ π β π») β (Β¬ π β π β (π β (πβ{π})) = π)) |
13 | 2, 12 | mpbid 231 |
. 2
β’ ((π β§ π β π») β (π β (πβ{π})) = π) |
14 | | lshpnel2.u |
. . . 4
β’ (π β π β π) |
15 | 14 | adantr 482 |
. . 3
β’ ((π β§ (π β (πβ{π})) = π) β π β π) |
16 | | lshpnel2.t |
. . . 4
β’ (π β π β π) |
17 | 16 | adantr 482 |
. . 3
β’ ((π β§ (π β (πβ{π})) = π) β π β π) |
18 | 10 | adantr 482 |
. . . 4
β’ ((π β§ (π β (πβ{π})) = π) β π β π) |
19 | | lveclmod 20583 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
20 | 7, 19 | syl 17 |
. . . . . . . . . 10
β’ (π β π β LMod) |
21 | | lshpnel2.s |
. . . . . . . . . . 11
β’ π = (LSubSpβπ) |
22 | 21, 4 | lspid 20459 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β (πβπ) = π) |
23 | 20, 14, 22 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβπ) = π) |
24 | 23 | uneq1d 4127 |
. . . . . . . 8
β’ (π β ((πβπ) βͺ (πβ{π})) = (π βͺ (πβ{π}))) |
25 | 24 | fveq2d 6851 |
. . . . . . 7
β’ (π β (πβ((πβπ) βͺ (πβ{π}))) = (πβ(π βͺ (πβ{π})))) |
26 | 3, 21 | lssss 20413 |
. . . . . . . . 9
β’ (π β π β π β π) |
27 | 14, 26 | syl 17 |
. . . . . . . 8
β’ (π β π β π) |
28 | 10 | snssd 4774 |
. . . . . . . 8
β’ (π β {π} β π) |
29 | 3, 4 | lspun 20464 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ {π} β π) β (πβ(π βͺ {π})) = (πβ((πβπ) βͺ (πβ{π})))) |
30 | 20, 27, 28, 29 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πβ(π βͺ {π})) = (πβ((πβπ) βͺ (πβ{π})))) |
31 | 3, 21, 4 | lspsncl 20454 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β (πβ{π}) β π) |
32 | 20, 10, 31 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πβ{π}) β π) |
33 | 21, 4, 5 | lsmsp 20563 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ (πβ{π}) β π) β (π β (πβ{π})) = (πβ(π βͺ (πβ{π})))) |
34 | 20, 14, 32, 33 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π β (πβ{π})) = (πβ(π βͺ (πβ{π})))) |
35 | 25, 30, 34 | 3eqtr4rd 2788 |
. . . . . 6
β’ (π β (π β (πβ{π})) = (πβ(π βͺ {π}))) |
36 | 35 | eqeq1d 2739 |
. . . . 5
β’ (π β ((π β (πβ{π})) = π β (πβ(π βͺ {π})) = π)) |
37 | 36 | biimpa 478 |
. . . 4
β’ ((π β§ (π β (πβ{π})) = π) β (πβ(π βͺ {π})) = π) |
38 | | sneq 4601 |
. . . . . . 7
β’ (π£ = π β {π£} = {π}) |
39 | 38 | uneq2d 4128 |
. . . . . 6
β’ (π£ = π β (π βͺ {π£}) = (π βͺ {π})) |
40 | 39 | fveqeq2d 6855 |
. . . . 5
β’ (π£ = π β ((πβ(π βͺ {π£})) = π β (πβ(π βͺ {π})) = π)) |
41 | 40 | rspcev 3584 |
. . . 4
β’ ((π β π β§ (πβ(π βͺ {π})) = π) β βπ£ β π (πβ(π βͺ {π£})) = π) |
42 | 18, 37, 41 | syl2anc 585 |
. . 3
β’ ((π β§ (π β (πβ{π})) = π) β βπ£ β π (πβ(π βͺ {π£})) = π) |
43 | 7 | adantr 482 |
. . . 4
β’ ((π β§ (π β (πβ{π})) = π) β π β LVec) |
44 | 3, 4, 21, 6 | islshp 37470 |
. . . 4
β’ (π β LVec β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
45 | 43, 44 | syl 17 |
. . 3
β’ ((π β§ (π β (πβ{π})) = π) β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
46 | 15, 17, 42, 45 | mpbir3and 1343 |
. 2
β’ ((π β§ (π β (πβ{π})) = π) β π β π») |
47 | 13, 46 | impbida 800 |
1
β’ (π β (π β π» β (π β (πβ{π})) = π)) |