Step | Hyp | Ref
| Expression |
1 | | lpolset.v |
. . . 4
β’ π = (Baseβπ) |
2 | | lpolset.s |
. . . 4
β’ π = (LSubSpβπ) |
3 | | lpolset.z |
. . . 4
β’ 0 =
(0gβπ) |
4 | | lpolset.a |
. . . 4
β’ π΄ = (LSAtomsβπ) |
5 | | lpolset.h |
. . . 4
β’ π» = (LSHypβπ) |
6 | | lpolset.p |
. . . 4
β’ π = (LPolβπ) |
7 | 1, 2, 3, 4, 5, 6 | lpolsetN 39995 |
. . 3
β’ (π β π β π = {π β (π βm π« π) β£ ((πβπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β§ βπ₯ β π΄ ((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯))}) |
8 | 7 | eleq2d 2820 |
. 2
β’ (π β π β ( β₯ β π β β₯ β {π β (π βm π« π) β£ ((πβπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β§ βπ₯ β π΄ ((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯))})) |
9 | | fveq1 6845 |
. . . . . 6
β’ (π = β₯ β (πβπ) = ( β₯ βπ)) |
10 | 9 | eqeq1d 2735 |
. . . . 5
β’ (π = β₯ β ((πβπ) = { 0 } β ( β₯
βπ) = { 0
})) |
11 | | fveq1 6845 |
. . . . . . . 8
β’ (π = β₯ β (πβπ¦) = ( β₯ βπ¦)) |
12 | | fveq1 6845 |
. . . . . . . 8
β’ (π = β₯ β (πβπ₯) = ( β₯ βπ₯)) |
13 | 11, 12 | sseq12d 3981 |
. . . . . . 7
β’ (π = β₯ β ((πβπ¦) β (πβπ₯) β ( β₯ βπ¦) β ( β₯ βπ₯))) |
14 | 13 | imbi2d 341 |
. . . . . 6
β’ (π = β₯ β (((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β ((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)))) |
15 | 14 | 2albidv 1927 |
. . . . 5
β’ (π = β₯ β
(βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)))) |
16 | 12 | eleq1d 2819 |
. . . . . . 7
β’ (π = β₯ β ((πβπ₯) β π» β ( β₯ βπ₯) β π»)) |
17 | | id 22 |
. . . . . . . . 9
β’ (π = β₯ β π = β₯ ) |
18 | 17, 12 | fveq12d 6853 |
. . . . . . . 8
β’ (π = β₯ β (πβ(πβπ₯)) = ( β₯ β( β₯
βπ₯))) |
19 | 18 | eqeq1d 2735 |
. . . . . . 7
β’ (π = β₯ β ((πβ(πβπ₯)) = π₯ β ( β₯ β( β₯
βπ₯)) = π₯)) |
20 | 16, 19 | anbi12d 632 |
. . . . . 6
β’ (π = β₯ β (((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯) β (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯))) |
21 | 20 | ralbidv 3171 |
. . . . 5
β’ (π = β₯ β
(βπ₯ β π΄ ((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯) β βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯))) |
22 | 10, 15, 21 | 3anbi123d 1437 |
. . . 4
β’ (π = β₯ β (((πβπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β§ βπ₯ β π΄ ((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯)) β (( β₯ βπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)) β§ βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯)))) |
23 | 22 | elrab 3649 |
. . 3
β’ ( β₯ β
{π β (π βm π«
π) β£ ((πβπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β§ βπ₯ β π΄ ((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯))} β ( β₯ β (π βm π«
π) β§ (( β₯
βπ) = { 0 } β§
βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)) β§ βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯)))) |
24 | 2 | fvexi 6860 |
. . . . 5
β’ π β V |
25 | 1 | fvexi 6860 |
. . . . . 6
β’ π β V |
26 | 25 | pwex 5339 |
. . . . 5
β’ π«
π β V |
27 | 24, 26 | elmap 8815 |
. . . 4
β’ ( β₯ β
(π βm
π« π) β β₯
:π« πβΆπ) |
28 | 27 | anbi1i 625 |
. . 3
β’ (( β₯ β
(π βm
π« π) β§ (( β₯
βπ) = { 0 } β§
βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)) β§ βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯))) β ( β₯ :π« πβΆπ β§ (( β₯ βπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)) β§ βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯)))) |
29 | 23, 28 | bitri 275 |
. 2
β’ ( β₯ β
{π β (π βm π«
π) β£ ((πβπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β (πβπ¦) β (πβπ₯)) β§ βπ₯ β π΄ ((πβπ₯) β π» β§ (πβ(πβπ₯)) = π₯))} β ( β₯ :π« πβΆπ β§ (( β₯ βπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)) β§ βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯)))) |
30 | 8, 29 | bitrdi 287 |
1
β’ (π β π β ( β₯ β π β ( β₯ :π« πβΆπ β§ (( β₯ βπ) = { 0 } β§ βπ₯βπ¦((π₯ β π β§ π¦ β π β§ π₯ β π¦) β ( β₯ βπ¦) β ( β₯ βπ₯)) β§ βπ₯ β π΄ (( β₯ βπ₯) β π» β§ ( β₯ β( β₯
βπ₯)) = π₯))))) |