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		df-base	⊢ Base = Slot 1
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 ↑ 𝑋 ) ) )