Step | Hyp | Ref
| Expression |
1 | | lbsext.a |
. . . . 5
β’ (π β π΄ β π) |
2 | | lbsext.s |
. . . . . 6
β’ π = {π§ β π« π β£ (πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})))} |
3 | 2 | ssrab3 4044 |
. . . . 5
β’ π β π« π |
4 | 1, 3 | sstrdi 3960 |
. . . 4
β’ (π β π΄ β π« π) |
5 | | sspwuni 5064 |
. . . 4
β’ (π΄ β π« π β βͺ π΄
β π) |
6 | 4, 5 | sylib 217 |
. . 3
β’ (π β βͺ π΄
β π) |
7 | | lbsext.v |
. . . . 5
β’ π = (Baseβπ) |
8 | 7 | fvexi 6860 |
. . . 4
β’ π β V |
9 | 8 | elpw2 5306 |
. . 3
β’ (βͺ π΄
β π« π β
βͺ π΄ β π) |
10 | 6, 9 | sylibr 233 |
. 2
β’ (π β βͺ π΄
β π« π) |
11 | | ssintub 4931 |
. . . . 5
β’ πΆ β β© {π§
β π« π β£
πΆ β π§} |
12 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯}))) β πΆ β π§) |
13 | 12 | a1i 11 |
. . . . . . . . 9
β’ (π§ β π« π β ((πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯}))) β πΆ β π§)) |
14 | 13 | ss2rabi 4038 |
. . . . . . . 8
β’ {π§ β π« π β£ (πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})))} β {π§ β π« π β£ πΆ β π§} |
15 | 2, 14 | eqsstri 3982 |
. . . . . . 7
β’ π β {π§ β π« π β£ πΆ β π§} |
16 | 1, 15 | sstrdi 3960 |
. . . . . 6
β’ (π β π΄ β {π§ β π« π β£ πΆ β π§}) |
17 | | intss 4934 |
. . . . . 6
β’ (π΄ β {π§ β π« π β£ πΆ β π§} β β© {π§ β π« π β£ πΆ β π§} β β© π΄) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (π β β© {π§
β π« π β£
πΆ β π§} β β© π΄) |
19 | 11, 18 | sstrid 3959 |
. . . 4
β’ (π β πΆ β β© π΄) |
20 | | lbsext.z |
. . . . 5
β’ (π β π΄ β β
) |
21 | | intssuni 4935 |
. . . . 5
β’ (π΄ β β
β β© π΄
β βͺ π΄) |
22 | 20, 21 | syl 17 |
. . . 4
β’ (π β β© π΄
β βͺ π΄) |
23 | 19, 22 | sstrd 3958 |
. . 3
β’ (π β πΆ β βͺ π΄) |
24 | | eluni2 4873 |
. . . . 5
β’ (π₯ β βͺ π΄
β βπ¦ β
π΄ π₯ β π¦) |
25 | | simpll1 1213 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π) |
26 | | lbsext.w |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
27 | | lveclmod 20611 |
. . . . . . . . . . . . 13
β’ (π β LVec β π β LMod) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β LMod) |
29 | 25, 28 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π β LMod) |
30 | 25, 1 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π΄ β π) |
31 | | lbsext.r |
. . . . . . . . . . . . . . . . 17
β’ (π β [β] Or π΄) |
32 | 25, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β [β] Or π΄) |
33 | | simpll2 1214 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π¦ β π΄) |
34 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π’ β π΄) |
35 | | sorpssun 7671 |
. . . . . . . . . . . . . . . 16
β’ ((
[β] Or π΄
β§ (π¦ β π΄ β§ π’ β π΄)) β (π¦ βͺ π’) β π΄) |
36 | 32, 33, 34, 35 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β (π¦ βͺ π’) β π΄) |
37 | 30, 36 | sseldd 3949 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β (π¦ βͺ π’) β π) |
38 | 3, 37 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β (π¦ βͺ π’) β π« π) |
39 | 38 | elpwid 4573 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β (π¦ βͺ π’) β π) |
40 | 39 | ssdifssd 4106 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β ((π¦ βͺ π’) β {π₯}) β π) |
41 | | ssun2 4137 |
. . . . . . . . . . . 12
β’ π’ β (π¦ βͺ π’) |
42 | | ssdif 4103 |
. . . . . . . . . . . 12
β’ (π’ β (π¦ βͺ π’) β (π’ β {π₯}) β ((π¦ βͺ π’) β {π₯})) |
43 | 41, 42 | mp1i 13 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β (π’ β {π₯}) β ((π¦ βͺ π’) β {π₯})) |
44 | | lbsext.n |
. . . . . . . . . . . 12
β’ π = (LSpanβπ) |
45 | 7, 44 | lspss 20489 |
. . . . . . . . . . 11
β’ ((π β LMod β§ ((π¦ βͺ π’) β {π₯}) β π β§ (π’ β {π₯}) β ((π¦ βͺ π’) β {π₯})) β (πβ(π’ β {π₯})) β (πβ((π¦ βͺ π’) β {π₯}))) |
46 | 29, 40, 43, 45 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β (πβ(π’ β {π₯})) β (πβ((π¦ βͺ π’) β {π₯}))) |
47 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π₯ β (πβ(π’ β {π₯}))) |
48 | 46, 47 | sseldd 3949 |
. . . . . . . . 9
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π₯ β (πβ((π¦ βͺ π’) β {π₯}))) |
49 | | sseq2 3974 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ π’) β (πΆ β π§ β πΆ β (π¦ βͺ π’))) |
50 | | difeq1 4079 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (π¦ βͺ π’) β (π§ β {π₯}) = ((π¦ βͺ π’) β {π₯})) |
51 | 50 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π¦ βͺ π’) β (πβ(π§ β {π₯})) = (πβ((π¦ βͺ π’) β {π₯}))) |
52 | 51 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π¦ βͺ π’) β (π₯ β (πβ(π§ β {π₯})) β π₯ β (πβ((π¦ βͺ π’) β {π₯})))) |
53 | 52 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π¦ βͺ π’) β (Β¬ π₯ β (πβ(π§ β {π₯})) β Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯})))) |
54 | 53 | raleqbi1dv 3306 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π¦ βͺ π’) β (βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})) β βπ₯ β (π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯})))) |
55 | 49, 54 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦ βͺ π’) β ((πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯}))) β (πΆ β (π¦ βͺ π’) β§ βπ₯ β (π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯}))))) |
56 | 55, 2 | elrab2 3652 |
. . . . . . . . . . . . 13
β’ ((π¦ βͺ π’) β π β ((π¦ βͺ π’) β π« π β§ (πΆ β (π¦ βͺ π’) β§ βπ₯ β (π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯}))))) |
57 | 56 | simprbi 498 |
. . . . . . . . . . . 12
β’ ((π¦ βͺ π’) β π β (πΆ β (π¦ βͺ π’) β§ βπ₯ β (π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯})))) |
58 | 57 | simprd 497 |
. . . . . . . . . . 11
β’ ((π¦ βͺ π’) β π β βπ₯ β (π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯}))) |
59 | 37, 58 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β βπ₯ β (π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯}))) |
60 | | simpll3 1215 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π₯ β π¦) |
61 | | elun1 4140 |
. . . . . . . . . . 11
β’ (π₯ β π¦ β π₯ β (π¦ βͺ π’)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β π₯ β (π¦ βͺ π’)) |
63 | | rsp 3229 |
. . . . . . . . . 10
β’
(βπ₯ β
(π¦ βͺ π’) Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯})) β (π₯ β (π¦ βͺ π’) β Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯})))) |
64 | 59, 62, 63 | sylc 65 |
. . . . . . . . 9
β’ ((((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β§ π₯ β (πβ(π’ β {π₯}))) β Β¬ π₯ β (πβ((π¦ βͺ π’) β {π₯}))) |
65 | 48, 64 | pm2.65da 816 |
. . . . . . . 8
β’ (((π β§ π¦ β π΄ β§ π₯ β π¦) β§ π’ β π΄) β Β¬ π₯ β (πβ(π’ β {π₯}))) |
66 | 65 | nrexdv 3143 |
. . . . . . 7
β’ ((π β§ π¦ β π΄ β§ π₯ β π¦) β Β¬ βπ’ β π΄ π₯ β (πβ(π’ β {π₯}))) |
67 | | lbsext.j |
. . . . . . . . . . . . . . . 16
β’ π½ = (LBasisβπ) |
68 | | lbsext.c |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ β π) |
69 | | lbsext.x |
. . . . . . . . . . . . . . . 16
β’ (π β βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯}))) |
70 | | lbsext.p |
. . . . . . . . . . . . . . . 16
β’ π = (LSubSpβπ) |
71 | | lbsext.t |
. . . . . . . . . . . . . . . 16
β’ π = βͺ π’ β π΄ (πβ(π’ β {π₯})) |
72 | 7, 67, 44, 26, 68, 69, 2, 70, 1, 20, 31, 71 | lbsextlem2 20665 |
. . . . . . . . . . . . . . 15
β’ (π β (π β π β§ (βͺ π΄ β {π₯}) β π)) |
73 | 72 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β π β π) |
74 | 7, 70 | lssss 20441 |
. . . . . . . . . . . . . 14
β’ (π β π β π β π) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
76 | 72 | simprd 497 |
. . . . . . . . . . . . 13
β’ (π β (βͺ π΄
β {π₯}) β π) |
77 | 7, 44 | lspss 20489 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π β§ (βͺ π΄ β {π₯}) β π) β (πβ(βͺ π΄ β {π₯})) β (πβπ)) |
78 | 28, 75, 76, 77 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (πβ(βͺ π΄ β {π₯})) β (πβπ)) |
79 | 70, 44 | lspid 20487 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π) β (πβπ) = π) |
80 | 28, 73, 79 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πβπ) = π) |
81 | 78, 80 | sseqtrd 3988 |
. . . . . . . . . . 11
β’ (π β (πβ(βͺ π΄ β {π₯})) β π) |
82 | 81 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄ β§ π₯ β π¦) β (πβ(βͺ π΄ β {π₯})) β π) |
83 | 82, 71 | sseqtrdi 3998 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΄ β§ π₯ β π¦) β (πβ(βͺ π΄ β {π₯})) β βͺ π’ β π΄ (πβ(π’ β {π₯}))) |
84 | 83 | sseld 3947 |
. . . . . . . 8
β’ ((π β§ π¦ β π΄ β§ π₯ β π¦) β (π₯ β (πβ(βͺ π΄ β {π₯})) β π₯ β βͺ
π’ β π΄ (πβ(π’ β {π₯})))) |
85 | | eliun 4962 |
. . . . . . . 8
β’ (π₯ β βͺ π’ β π΄ (πβ(π’ β {π₯})) β βπ’ β π΄ π₯ β (πβ(π’ β {π₯}))) |
86 | 84, 85 | syl6ib 251 |
. . . . . . 7
β’ ((π β§ π¦ β π΄ β§ π₯ β π¦) β (π₯ β (πβ(βͺ π΄ β {π₯})) β βπ’ β π΄ π₯ β (πβ(π’ β {π₯})))) |
87 | 66, 86 | mtod 197 |
. . . . . 6
β’ ((π β§ π¦ β π΄ β§ π₯ β π¦) β Β¬ π₯ β (πβ(βͺ π΄ β {π₯}))) |
88 | 87 | rexlimdv3a 3153 |
. . . . 5
β’ (π β (βπ¦ β π΄ π₯ β π¦ β Β¬ π₯ β (πβ(βͺ π΄ β {π₯})))) |
89 | 24, 88 | biimtrid 241 |
. . . 4
β’ (π β (π₯ β βͺ π΄ β Β¬ π₯ β (πβ(βͺ π΄ β {π₯})))) |
90 | 89 | ralrimiv 3139 |
. . 3
β’ (π β βπ₯ β βͺ π΄ Β¬ π₯ β (πβ(βͺ π΄ β {π₯}))) |
91 | 23, 90 | jca 513 |
. 2
β’ (π β (πΆ β βͺ π΄ β§ βπ₯ β βͺ π΄
Β¬ π₯ β (πβ(βͺ π΄
β {π₯})))) |
92 | | sseq2 3974 |
. . . 4
β’ (π§ = βͺ
π΄ β (πΆ β π§ β πΆ β βͺ π΄)) |
93 | | difeq1 4079 |
. . . . . . . 8
β’ (π§ = βͺ
π΄ β (π§ β {π₯}) = (βͺ π΄ β {π₯})) |
94 | 93 | fveq2d 6850 |
. . . . . . 7
β’ (π§ = βͺ
π΄ β (πβ(π§ β {π₯})) = (πβ(βͺ π΄ β {π₯}))) |
95 | 94 | eleq2d 2820 |
. . . . . 6
β’ (π§ = βͺ
π΄ β (π₯ β (πβ(π§ β {π₯})) β π₯ β (πβ(βͺ π΄ β {π₯})))) |
96 | 95 | notbid 318 |
. . . . 5
β’ (π§ = βͺ
π΄ β (Β¬ π₯ β (πβ(π§ β {π₯})) β Β¬ π₯ β (πβ(βͺ π΄ β {π₯})))) |
97 | 96 | raleqbi1dv 3306 |
. . . 4
β’ (π§ = βͺ
π΄ β (βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})) β βπ₯ β βͺ π΄ Β¬ π₯ β (πβ(βͺ π΄ β {π₯})))) |
98 | 92, 97 | anbi12d 632 |
. . 3
β’ (π§ = βͺ
π΄ β ((πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯}))) β (πΆ β βͺ π΄ β§ βπ₯ β βͺ π΄
Β¬ π₯ β (πβ(βͺ π΄
β {π₯}))))) |
99 | 98, 2 | elrab2 3652 |
. 2
β’ (βͺ π΄
β π β (βͺ π΄
β π« π β§
(πΆ β βͺ π΄
β§ βπ₯ β
βͺ π΄ Β¬ π₯ β (πβ(βͺ π΄ β {π₯}))))) |
100 | 10, 91, 99 | sylanbrc 584 |
1
β’ (π β βͺ π΄
β π) |