Metamath Proof Explorer

Theorem ply1idvr1OLD

Description: Obsolete version of ply1idvr1 as of 3-Jul-2025. (Contributed by AV, 14-Aug-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ply1idvr1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1idvr1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
ply1idvr1.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
ply1idvr1.e ⊢ ↑ = ( .g ‘ 𝑁 )
Assertion ply1idvr1OLD ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )

Proof

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 ‘ 𝑃 ) )