Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
2 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ถโ๐) = (๐ถโ๐)) |
3 | 1, 2 | eqeq12d 2749 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ดโ๐) = (๐ถโ๐) โ (๐ดโ๐) = (๐ถโ๐))) |
4 | 3 | rspccv 3577 |
. . . . . . . . 9
โข
(โ๐ โ
โ0 (๐ดโ๐) = (๐ถโ๐) โ (๐ โ โ0 โ (๐ดโ๐) = (๐ถโ๐))) |
5 | 4 | adantl 483 |
. . . . . . . 8
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โ (๐ โ โ0 โ (๐ดโ๐) = (๐ถโ๐))) |
6 | 5 | imp 408 |
. . . . . . 7
โข ((((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โง ๐ โ โ0) โ (๐ดโ๐) = (๐ถโ๐)) |
7 | | eqcoe1ply1eq.a |
. . . . . . . 8
โข ๐ด = (coe1โ๐พ) |
8 | 7 | fveq1i 6844 |
. . . . . . 7
โข (๐ดโ๐) = ((coe1โ๐พ)โ๐) |
9 | | eqcoe1ply1eq.c |
. . . . . . . 8
โข ๐ถ = (coe1โ๐ฟ) |
10 | 9 | fveq1i 6844 |
. . . . . . 7
โข (๐ถโ๐) = ((coe1โ๐ฟ)โ๐) |
11 | 6, 8, 10 | 3eqtr3g 2796 |
. . . . . 6
โข ((((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โง ๐ โ โ0) โ
((coe1โ๐พ)โ๐) = ((coe1โ๐ฟ)โ๐)) |
12 | 11 | oveq1d 7373 |
. . . . 5
โข ((((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โง ๐ โ โ0) โ
(((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) =
(((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) |
13 | 12 | mpteq2dva 5206 |
. . . 4
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โ (๐ โ โ0 โฆ
(((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) = (๐ โ โ0 โฆ
(((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) |
14 | 13 | oveq2d 7374 |
. . 3
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โ (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
15 | | eqcoe1ply1eq.p |
. . . . . . 7
โข ๐ = (Poly1โ๐
) |
16 | | eqid 2733 |
. . . . . . 7
โข
(var1โ๐
) = (var1โ๐
) |
17 | | eqcoe1ply1eq.b |
. . . . . . 7
โข ๐ต = (Baseโ๐) |
18 | | eqid 2733 |
. . . . . . 7
โข (
ยท๐ โ๐) = ( ยท๐
โ๐) |
19 | | eqid 2733 |
. . . . . . 7
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
20 | | eqid 2733 |
. . . . . . 7
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ๐)) |
21 | | eqid 2733 |
. . . . . . 7
โข
(coe1โ๐พ) = (coe1โ๐พ) |
22 | 15, 16, 17, 18, 19, 20, 21 | ply1coe 21683 |
. . . . . 6
โข ((๐
โ Ring โง ๐พ โ ๐ต) โ ๐พ = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
23 | 22 | 3adant3 1133 |
. . . . 5
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ๐พ = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
24 | | eqid 2733 |
. . . . . . 7
โข
(coe1โ๐ฟ) = (coe1โ๐ฟ) |
25 | 15, 16, 17, 18, 19, 20, 24 | ply1coe 21683 |
. . . . . 6
โข ((๐
โ Ring โง ๐ฟ โ ๐ต) โ ๐ฟ = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
26 | 25 | 3adant2 1132 |
. . . . 5
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ๐ฟ = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
27 | 23, 26 | eqeq12d 2749 |
. . . 4
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (๐พ = ๐ฟ โ (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
28 | 27 | adantr 482 |
. . 3
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โ (๐พ = ๐ฟ โ (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐พ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ๐ฟ)โ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
29 | 14, 28 | mpbird 257 |
. 2
โข (((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โง โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐)) โ ๐พ = ๐ฟ) |
30 | 29 | ex 414 |
1
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (โ๐ โ โ0 (๐ดโ๐) = (๐ถโ๐) โ ๐พ = ๐ฟ)) |