Metamath Proof Explorer


Theorem ply1scltm

Description: A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses ply1scltm.k 𝐾 = ( Base ‘ 𝑅 )
ply1scltm.p 𝑃 = ( Poly1𝑅 )
ply1scltm.x 𝑋 = ( var1𝑅 )
ply1scltm.m · = ( ·𝑠𝑃 )
ply1scltm.n 𝑁 = ( mulGrp ‘ 𝑃 )
ply1scltm.e = ( .g𝑁 )
ply1scltm.a 𝐴 = ( algSc ‘ 𝑃 )
Assertion ply1scltm ( ( 𝑅 ∈ Ring ∧ 𝐹𝐾 ) → ( 𝐴𝐹 ) = ( 𝐹 · ( 0 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 ply1scltm.k 𝐾 = ( Base ‘ 𝑅 )
2 ply1scltm.p 𝑃 = ( Poly1𝑅 )
3 ply1scltm.x 𝑋 = ( var1𝑅 )
4 ply1scltm.m · = ( ·𝑠𝑃 )
5 ply1scltm.n 𝑁 = ( mulGrp ‘ 𝑃 )
6 ply1scltm.e = ( .g𝑁 )
7 ply1scltm.a 𝐴 = ( algSc ‘ 𝑃 )
8 2 ply1sca2 ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )
9 baseid Base = Slot ( Base ‘ ndx )
10 9 1 strfvi 𝐾 = ( Base ‘ ( I ‘ 𝑅 ) )
11 eqid ( 1r𝑃 ) = ( 1r𝑃 )
12 7 8 10 4 11 asclval ( 𝐹𝐾 → ( 𝐴𝐹 ) = ( 𝐹 · ( 1r𝑃 ) ) )
13 12 adantl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐾 ) → ( 𝐴𝐹 ) = ( 𝐹 · ( 1r𝑃 ) ) )
14 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15 3 2 14 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
16 5 14 mgpbas ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 )
17 5 11 ringidval ( 1r𝑃 ) = ( 0g𝑁 )
18 16 17 6 mulg0 ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 𝑋 ) = ( 1r𝑃 ) )
19 15 18 syl ( 𝑅 ∈ Ring → ( 0 𝑋 ) = ( 1r𝑃 ) )
20 19 adantr ( ( 𝑅 ∈ Ring ∧ 𝐹𝐾 ) → ( 0 𝑋 ) = ( 1r𝑃 ) )
21 20 oveq2d ( ( 𝑅 ∈ Ring ∧ 𝐹𝐾 ) → ( 𝐹 · ( 0 𝑋 ) ) = ( 𝐹 · ( 1r𝑃 ) ) )
22 13 21 eqtr4d ( ( 𝑅 ∈ Ring ∧ 𝐹𝐾 ) → ( 𝐴𝐹 ) = ( 𝐹 · ( 0 𝑋 ) ) )