Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. 2
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ ๐ โ โ) |
2 | | simp2 1135 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ ๐ โ
โ0) |
3 | | simp3 1136 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ ๐ด:โ0โถ๐) |
4 | | ssun1 4173 |
. . . . 5
โข ๐ โ (๐ โช {0}) |
5 | | fss 6735 |
. . . . 5
โข ((๐ด:โ0โถ๐ โง ๐ โ (๐ โช {0})) โ ๐ด:โ0โถ(๐ โช {0})) |
6 | 3, 4, 5 | sylancl 584 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ ๐ด:โ0โถ(๐ โช {0})) |
7 | | 0cnd 11213 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ 0 โ
โ) |
8 | 7 | snssd 4813 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ {0} โ
โ) |
9 | 1, 8 | unssd 4187 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ (๐ โช {0}) โ
โ) |
10 | | cnex 11195 |
. . . . . 6
โข โ
โ V |
11 | | ssexg 5324 |
. . . . . 6
โข (((๐ โช {0}) โ โ
โง โ โ V) โ (๐ โช {0}) โ V) |
12 | 9, 10, 11 | sylancl 584 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ (๐ โช {0}) โ V) |
13 | | nn0ex 12484 |
. . . . 5
โข
โ0 โ V |
14 | | elmapg 8837 |
. . . . 5
โข (((๐ โช {0}) โ V โง
โ0 โ V) โ (๐ด โ ((๐ โช {0}) โm
โ0) โ ๐ด:โ0โถ(๐ โช {0}))) |
15 | 12, 13, 14 | sylancl 584 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ (๐ด โ ((๐ โช {0}) โm
โ0) โ ๐ด:โ0โถ(๐ โช {0}))) |
16 | 6, 15 | mpbird 256 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ ๐ด โ ((๐ โช {0}) โm
โ0)) |
17 | | eqidd 2731 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐)))) |
18 | | oveq2 7421 |
. . . . . . 7
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
19 | 18 | sumeq1d 15653 |
. . . . . 6
โข (๐ = ๐ โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
20 | 19 | mpteq2dv 5251 |
. . . . 5
โข (๐ = ๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
21 | 20 | eqeq2d 2741 |
. . . 4
โข (๐ = ๐ โ ((๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
22 | | fveq1 6891 |
. . . . . . . 8
โข (๐ = ๐ด โ (๐โ๐) = (๐ดโ๐)) |
23 | 22 | oveq1d 7428 |
. . . . . . 7
โข (๐ = ๐ด โ ((๐โ๐) ยท (๐งโ๐)) = ((๐ดโ๐) ยท (๐งโ๐))) |
24 | 23 | sumeq2sdv 15656 |
. . . . . 6
โข (๐ = ๐ด โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) |
25 | 24 | mpteq2dv 5251 |
. . . . 5
โข (๐ = ๐ด โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐)))) |
26 | 25 | eqeq2d 2741 |
. . . 4
โข (๐ = ๐ด โ ((๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))))) |
27 | 21, 26 | rspc2ev 3625 |
. . 3
โข ((๐ โ โ0
โง ๐ด โ ((๐ โช {0}) โm
โ0) โง (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐)))) โ โ๐ โ โ0 โ๐ โ ((๐ โช {0}) โm
โ0)(๐ง
โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
28 | 2, 16, 17, 27 | syl3anc 1369 |
. 2
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ โ๐ โ โ0
โ๐ โ ((๐ โช {0}) โm
โ0)(๐ง
โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
29 | | elply 25943 |
. 2
โข ((๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) โ (Polyโ๐) โ (๐ โ โ โง โ๐ โ โ0
โ๐ โ ((๐ โช {0}) โm
โ0)(๐ง
โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
30 | 1, 28, 29 | sylanbrc 581 |
1
โข ((๐ โ โ โง ๐ โ โ0
โง ๐ด:โ0โถ๐) โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐ดโ๐) ยท (๐งโ๐))) โ (Polyโ๐)) |