Description: The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019) (Proof shortened by SN, 3-Jul-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply1idvr1.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
ply1idvr1.x | ⊢ 𝑋 = ( var1 ‘ 𝑅 ) | ||
ply1idvr1.n | ⊢ 𝑁 = ( mulGrp ‘ 𝑃 ) | ||
ply1idvr1.e | ⊢ ↑ = ( .g ‘ 𝑁 ) | ||
Assertion | ply1idvr1 | ⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1idvr1.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
2 | ply1idvr1.x | ⊢ 𝑋 = ( var1 ‘ 𝑅 ) | |
3 | ply1idvr1.n | ⊢ 𝑁 = ( mulGrp ‘ 𝑃 ) | |
4 | ply1idvr1.e | ⊢ ↑ = ( .g ‘ 𝑁 ) | |
5 | eqid | ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) | |
6 | 2 1 5 | vr1cl | ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
7 | 3 5 | mgpbas | ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 ) |
8 | eqid | ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 ) | |
9 | 3 8 | ringidval | ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑁 ) |
10 | 7 9 4 | mulg0 | ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) ) |
11 | 6 10 | syl | ⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) ) |