Step | Hyp | Ref
| Expression |
1 | | elex 3466 |
. 2
β’ (πΎ β π΄ β πΎ β V) |
2 | | lplnset.p |
. . 3
β’ π = (LPlanesβπΎ) |
3 | | fveq2 6847 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | lplnset.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | | fveq2 6847 |
. . . . . . 7
β’ (π = πΎ β (LLinesβπ) = (LLinesβπΎ)) |
7 | | lplnset.n |
. . . . . . 7
β’ π = (LLinesβπΎ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
β’ (π = πΎ β (LLinesβπ) = π) |
9 | | fveq2 6847 |
. . . . . . . 8
β’ (π = πΎ β ( β βπ) = ( β βπΎ)) |
10 | | lplnset.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β ( β βπ) = πΆ) |
12 | 11 | breqd 5121 |
. . . . . 6
β’ (π = πΎ β (π¦( β βπ)π₯ β π¦πΆπ₯)) |
13 | 8, 12 | rexeqbidv 3323 |
. . . . 5
β’ (π = πΎ β (βπ¦ β (LLinesβπ)π¦( β βπ)π₯ β βπ¦ β π π¦πΆπ₯)) |
14 | 5, 13 | rabeqbidv 3427 |
. . . 4
β’ (π = πΎ β {π₯ β (Baseβπ) β£ βπ¦ β (LLinesβπ)π¦( β βπ)π₯} = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |
15 | | df-lplanes 37991 |
. . . 4
β’ LPlanes =
(π β V β¦ {π₯ β (Baseβπ) β£ βπ¦ β (LLinesβπ)π¦( β βπ)π₯}) |
16 | 4 | fvexi 6861 |
. . . . 5
β’ π΅ β V |
17 | 16 | rabex 5294 |
. . . 4
β’ {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯} β V |
18 | 14, 15, 17 | fvmpt 6953 |
. . 3
β’ (πΎ β V β
(LPlanesβπΎ) = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |
19 | 2, 18 | eqtrid 2789 |
. 2
β’ (πΎ β V β π = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |
20 | 1, 19 | syl 17 |
1
β’ (πΎ β π΄ β π = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |