Step | Hyp | Ref
| Expression |
1 | | axcontlem1.1 |
. 2
โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} |
2 | | eleq1w 2816 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ฅ โ ๐ท โ ๐ฆ โ ๐ท)) |
3 | 2 | adantr 481 |
. . . 4
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ (๐ฅ โ ๐ท โ ๐ฆ โ ๐ท)) |
4 | | eleq1w 2816 |
. . . . . 6
โข (๐ก = ๐ โ (๐ก โ (0[,)+โ) โ ๐ โ
(0[,)+โ))) |
5 | 4 | adantl 482 |
. . . . 5
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ (๐ก โ (0[,)+โ) โ ๐ โ
(0[,)+โ))) |
6 | | fveq1 6890 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ (๐ฅโ๐) = (๐ฆโ๐)) |
7 | | oveq2 7419 |
. . . . . . . . . 10
โข (๐ก = ๐ โ (1 โ ๐ก) = (1 โ ๐ )) |
8 | 7 | oveq1d 7426 |
. . . . . . . . 9
โข (๐ก = ๐ โ ((1 โ ๐ก) ยท (๐โ๐)) = ((1 โ ๐ ) ยท (๐โ๐))) |
9 | | oveq1 7418 |
. . . . . . . . 9
โข (๐ก = ๐ โ (๐ก ยท (๐โ๐)) = (๐ ยท (๐โ๐))) |
10 | 8, 9 | oveq12d 7429 |
. . . . . . . 8
โข (๐ก = ๐ โ (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) |
11 | 6, 10 | eqeqan12d 2746 |
. . . . . . 7
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ ((๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ (๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
12 | 11 | ralbidv 3177 |
. . . . . 6
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ (โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
13 | | fveq2 6891 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ฆโ๐) = (๐ฆโ๐)) |
14 | | fveq2 6891 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
15 | 14 | oveq2d 7427 |
. . . . . . . . 9
โข (๐ = ๐ โ ((1 โ ๐ ) ยท (๐โ๐)) = ((1 โ ๐ ) ยท (๐โ๐))) |
16 | | fveq2 6891 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
17 | 16 | oveq2d 7427 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท (๐โ๐)) = (๐ ยท (๐โ๐))) |
18 | 15, 17 | oveq12d 7429 |
. . . . . . . 8
โข (๐ = ๐ โ (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) |
19 | 13, 18 | eqeq12d 2748 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))) โ (๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
20 | 19 | cbvralvw 3234 |
. . . . . 6
โข
(โ๐ โ
(1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))) โ โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))) |
21 | 12, 20 | bitrdi 286 |
. . . . 5
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ (โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))) โ โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))) |
22 | 5, 21 | anbi12d 631 |
. . . 4
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ ((๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))) โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) |
23 | 3, 22 | anbi12d 631 |
. . 3
โข ((๐ฅ = ๐ฆ โง ๐ก = ๐ ) โ ((๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐))))) โ (๐ฆ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐))))))) |
24 | 23 | cbvopabv 5221 |
. 2
โข
{โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} = {โจ๐ฆ, ๐ โฉ โฃ (๐ฆ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))} |
25 | 1, 24 | eqtri 2760 |
1
โข ๐น = {โจ๐ฆ, ๐ โฉ โฃ (๐ฆ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))} |