This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↑ 𝑋 ) ) )