Step | Hyp | Ref
| Expression |
1 | | elex 3462 |
. 2
β’ (πΎ β π· β πΎ β V) |
2 | | patoms.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
3 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | patoms.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β ( β βπ) = ( β βπΎ)) |
7 | | patoms.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β ( β βπ) = πΆ) |
9 | 8 | breqd 5117 |
. . . . . 6
β’ (π = πΎ β ((0.βπ)( β βπ)π₯ β (0.βπ)πΆπ₯)) |
10 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (0.βπ) = (0.βπΎ)) |
11 | | patoms.z |
. . . . . . . 8
β’ 0 =
(0.βπΎ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (0.βπ) = 0 ) |
13 | 12 | breq1d 5116 |
. . . . . 6
β’ (π = πΎ β ((0.βπ)πΆπ₯ β 0 πΆπ₯)) |
14 | 9, 13 | bitrd 279 |
. . . . 5
β’ (π = πΎ β ((0.βπ)( β βπ)π₯ β 0 πΆπ₯)) |
15 | 5, 14 | rabeqbidv 3423 |
. . . 4
β’ (π = πΎ β {π₯ β (Baseβπ) β£ (0.βπ)( β βπ)π₯} = {π₯ β π΅ β£ 0 πΆπ₯}) |
16 | | df-ats 37775 |
. . . 4
β’ Atoms =
(π β V β¦ {π₯ β (Baseβπ) β£ (0.βπ)( β βπ)π₯}) |
17 | 4 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
18 | 17 | rabex 5290 |
. . . 4
β’ {π₯ β π΅ β£ 0 πΆπ₯} β V |
19 | 15, 16, 18 | fvmpt 6949 |
. . 3
β’ (πΎ β V β
(AtomsβπΎ) = {π₯ β π΅ β£ 0 πΆπ₯}) |
20 | 2, 19 | eqtrid 2785 |
. 2
β’ (πΎ β V β π΄ = {π₯ β π΅ β£ 0 πΆπ₯}) |
21 | 1, 20 | syl 17 |
1
β’ (πΎ β π· β π΄ = {π₯ β π΅ β£ 0 πΆπ₯}) |