Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | psubspset.s |
. . 3
β’ π = (PSubSpβπΎ) |
3 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
4 | | psubspset.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = π΄) |
6 | 5 | sseq2d 3980 |
. . . . . 6
β’ (π = πΎ β (π β (Atomsβπ) β π β π΄)) |
7 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
8 | | psubspset.j |
. . . . . . . . . . . . 13
β’ β¨ =
(joinβπΎ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π = πΎ β (joinβπ) = β¨ ) |
10 | 9 | oveqd 7378 |
. . . . . . . . . . 11
β’ (π = πΎ β (π(joinβπ)π) = (π β¨ π)) |
11 | 10 | breq2d 5121 |
. . . . . . . . . 10
β’ (π = πΎ β (π(leβπ)(π(joinβπ)π) β π(leβπ)(π β¨ π))) |
12 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
13 | | psubspset.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = β€ ) |
15 | 14 | breqd 5120 |
. . . . . . . . . 10
β’ (π = πΎ β (π(leβπ)(π β¨ π) β π β€ (π β¨ π))) |
16 | 11, 15 | bitrd 279 |
. . . . . . . . 9
β’ (π = πΎ β (π(leβπ)(π(joinβπ)π) β π β€ (π β¨ π))) |
17 | 16 | imbi1d 342 |
. . . . . . . 8
β’ (π = πΎ β ((π(leβπ)(π(joinβπ)π) β π β π ) β (π β€ (π β¨ π) β π β π ))) |
18 | 5, 17 | raleqbidv 3318 |
. . . . . . 7
β’ (π = πΎ β (βπ β (Atomsβπ)(π(leβπ)(π(joinβπ)π) β π β π ) β βπ β π΄ (π β€ (π β¨ π) β π β π ))) |
19 | 18 | 2ralbidv 3209 |
. . . . . 6
β’ (π = πΎ β (βπ β π βπ β π βπ β (Atomsβπ)(π(leβπ)(π(joinβπ)π) β π β π ) β βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))) |
20 | 6, 19 | anbi12d 632 |
. . . . 5
β’ (π = πΎ β ((π β (Atomsβπ) β§ βπ β π βπ β π βπ β (Atomsβπ)(π(leβπ)(π(joinβπ)π) β π β π )) β (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π )))) |
21 | 20 | abbidv 2802 |
. . . 4
β’ (π = πΎ β {π β£ (π β (Atomsβπ) β§ βπ β π βπ β π βπ β (Atomsβπ)(π(leβπ)(π(joinβπ)π) β π β π ))} = {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))}) |
22 | | df-psubsp 38016 |
. . . 4
β’ PSubSp =
(π β V β¦ {π β£ (π β (Atomsβπ) β§ βπ β π βπ β π βπ β (Atomsβπ)(π(leβπ)(π(joinβπ)π) β π β π ))}) |
23 | 4 | fvexi 6860 |
. . . . . 6
β’ π΄ β V |
24 | 23 | pwex 5339 |
. . . . 5
β’ π«
π΄ β V |
25 | | velpw 4569 |
. . . . . . . 8
β’ (π β π« π΄ β π β π΄) |
26 | 25 | anbi1i 625 |
. . . . . . 7
β’ ((π β π« π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π )) β (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))) |
27 | 26 | abbii 2803 |
. . . . . 6
β’ {π β£ (π β π« π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))} = {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))} |
28 | | ssab2 4040 |
. . . . . 6
β’ {π β£ (π β π« π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))} β π« π΄ |
29 | 27, 28 | eqsstrri 3983 |
. . . . 5
β’ {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))} β π« π΄ |
30 | 24, 29 | ssexi 5283 |
. . . 4
β’ {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))} β V |
31 | 21, 22, 30 | fvmpt 6952 |
. . 3
β’ (πΎ β V β
(PSubSpβπΎ) = {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))}) |
32 | 2, 31 | eqtrid 2785 |
. 2
β’ (πΎ β V β π = {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))}) |
33 | 1, 32 | syl 17 |
1
β’ (πΎ β π΅ β π = {π β£ (π β π΄ β§ βπ β π βπ β π βπ β π΄ (π β€ (π β¨ π) β π β π ))}) |