Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π΄ β πΎ β V) |
2 | | lvolset.v |
. . 3
β’ π = (LVolsβπΎ) |
3 | | fveq2 6846 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | lvolset.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (LPlanesβπ) = (LPlanesβπΎ)) |
7 | | lvolset.p |
. . . . . . 7
β’ π = (LPlanesβπΎ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (LPlanesβπ) = π) |
9 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β ( β βπ) = ( β βπΎ)) |
10 | | lvolset.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β ( β βπ) = πΆ) |
12 | 11 | breqd 5120 |
. . . . . 6
β’ (π = πΎ β (π¦( β βπ)π₯ β π¦πΆπ₯)) |
13 | 8, 12 | rexeqbidv 3319 |
. . . . 5
β’ (π = πΎ β (βπ¦ β (LPlanesβπ)π¦( β βπ)π₯ β βπ¦ β π π¦πΆπ₯)) |
14 | 5, 13 | rabeqbidv 3423 |
. . . 4
β’ (π = πΎ β {π₯ β (Baseβπ) β£ βπ¦ β (LPlanesβπ)π¦( β βπ)π₯} = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |
15 | | df-lvols 38013 |
. . . 4
β’ LVols =
(π β V β¦ {π₯ β (Baseβπ) β£ βπ¦ β (LPlanesβπ)π¦( β βπ)π₯}) |
16 | 4 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
17 | 16 | rabex 5293 |
. . . 4
β’ {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯} β V |
18 | 14, 15, 17 | fvmpt 6952 |
. . 3
β’ (πΎ β V β
(LVolsβπΎ) = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |
19 | 2, 18 | eqtrid 2785 |
. 2
β’ (πΎ β V β π = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |
20 | 1, 19 | syl 17 |
1
β’ (πΎ β π΄ β π = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) |