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 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
7 |
5 6
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
8 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 ) |
9 |
|
eqid |
⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 ) |
10 |
5 1 2 8 3 4 9
|
ply1scltm |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) ) |
11 |
7 10
|
mpdan |
⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) ) |
12 |
1
|
ply1sca |
⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) ) |
13 |
12
|
fveq2d |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) |
14 |
13
|
oveq1d |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) ) |
15 |
1
|
ply1lmod |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod ) |
16 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
17 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
18 |
1 2 3 4 17
|
ply1moncl |
⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ ℕ0 ) → ( 0 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) |
19 |
16 18
|
mpan2 |
⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) |
20 |
|
eqid |
⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 ) |
21 |
|
eqid |
⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) |
22 |
17 20 8 21
|
lmodvs1 |
⊢ ( ( 𝑃 ∈ LMod ∧ ( 0 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) = ( 0 ↑ 𝑋 ) ) |
23 |
15 19 22
|
syl2anc |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) = ( 0 ↑ 𝑋 ) ) |
24 |
11 14 23
|
3eqtrrd |
⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) |
25 |
|
eqid |
⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 ) |
26 |
1 9 6 25
|
ply1scl1 |
⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) ) |
27 |
24 26
|
eqtrd |
⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) ) |