Step | Hyp | Ref
| Expression |
1 | | cntzfval.z |
. 2
โข ๐ = (Cntzโ๐) |
2 | | elex 3466 |
. . 3
โข (๐ โ ๐ โ ๐ โ V) |
3 | | fveq2 6847 |
. . . . . . 7
โข (๐ = ๐ โ (Baseโ๐) = (Baseโ๐)) |
4 | | cntzfval.b |
. . . . . . 7
โข ๐ต = (Baseโ๐) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . 6
โข (๐ = ๐ โ (Baseโ๐) = ๐ต) |
6 | 5 | pweqd 4582 |
. . . . 5
โข (๐ = ๐ โ ๐ซ (Baseโ๐) = ๐ซ ๐ต) |
7 | | fveq2 6847 |
. . . . . . . . . 10
โข (๐ = ๐ โ (+gโ๐) = (+gโ๐)) |
8 | | cntzfval.p |
. . . . . . . . . 10
โข + =
(+gโ๐) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . 9
โข (๐ = ๐ โ (+gโ๐) = + ) |
10 | 9 | oveqd 7379 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ฅ(+gโ๐)๐ฆ) = (๐ฅ + ๐ฆ)) |
11 | 9 | oveqd 7379 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ฆ(+gโ๐)๐ฅ) = (๐ฆ + ๐ฅ)) |
12 | 10, 11 | eqeq12d 2753 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ))) |
13 | 12 | ralbidv 3175 |
. . . . . 6
โข (๐ = ๐ โ (โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ))) |
14 | 5, 13 | rabeqbidv 3427 |
. . . . 5
โข (๐ = ๐ โ {๐ฅ โ (Baseโ๐) โฃ โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)} = {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)}) |
15 | 6, 14 | mpteq12dv 5201 |
. . . 4
โข (๐ = ๐ โ (๐ โ ๐ซ (Baseโ๐) โฆ {๐ฅ โ (Baseโ๐) โฃ โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)}) = (๐ โ ๐ซ ๐ต โฆ {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)})) |
16 | | df-cntz 19104 |
. . . 4
โข Cntz =
(๐ โ V โฆ (๐ โ ๐ซ
(Baseโ๐) โฆ
{๐ฅ โ (Baseโ๐) โฃ โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)})) |
17 | 4 | fvexi 6861 |
. . . . . 6
โข ๐ต โ V |
18 | 17 | pwex 5340 |
. . . . 5
โข ๐ซ
๐ต โ V |
19 | 18 | mptex 7178 |
. . . 4
โข (๐ โ ๐ซ ๐ต โฆ {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)}) โ V |
20 | 15, 16, 19 | fvmpt 6953 |
. . 3
โข (๐ โ V โ
(Cntzโ๐) = (๐ โ ๐ซ ๐ต โฆ {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)})) |
21 | 2, 20 | syl 17 |
. 2
โข (๐ โ ๐ โ (Cntzโ๐) = (๐ โ ๐ซ ๐ต โฆ {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)})) |
22 | 1, 21 | eqtrid 2789 |
1
โข (๐ โ ๐ โ ๐ = (๐ โ ๐ซ ๐ต โฆ {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)})) |