Theorem ply1vr1smo

Description: The variable in a polynomial expressed as scaled monomial. (Contributed by AV, 12-Aug-2019)

	Ref	Expression
Hypotheses	ply1vr1smo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1vr1smo.i	⊢ 1 = ( 1r ‘ 𝑅 )
	ply1vr1smo.t	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1vr1smo.m	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	ply1vr1smo.e	⊢ ↑ = ( .g ‘ 𝐺 )
	ply1vr1smo.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion	ply1vr1smo	⊢ ( 𝑅 ∈ Ring → ( 1 · ( 1 ↑ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ply1vr1smo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1vr1smo.i	⊢ 1 = ( 1r ‘ 𝑅 )
3		ply1vr1smo.t	⊢ · = ( ·𝑠 ‘ 𝑃 )
4		ply1vr1smo.m	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
5		ply1vr1smo.e	⊢ ↑ = ( .g ‘ 𝐺 )
6		ply1vr1smo.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
8	7	fveq2d	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
9	2 8	eqtrid	⊢ ( 𝑅 ∈ Ring → 1 = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
10	9	oveq1d	⊢ ( 𝑅 ∈ Ring → ( 1 · ( 1 ↑ 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) · ( 1 ↑ 𝑋 ) ) )
11	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
12		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
13	6 1 12	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
14	4 12	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
15	14 5	mulg1	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 1 ↑ 𝑋 ) = 𝑋 )
16	13 15	syl	⊢ ( 𝑅 ∈ Ring → ( 1 ↑ 𝑋 ) = 𝑋 )
17	16 13	eqeltrd	⊢ ( 𝑅 ∈ Ring → ( 1 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
18		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
19		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
20	12 18 3 19	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 1 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) · ( 1 ↑ 𝑋 ) ) = ( 1 ↑ 𝑋 ) )
21	11 17 20	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) · ( 1 ↑ 𝑋 ) ) = ( 1 ↑ 𝑋 ) )
22	10 21 16	3eqtrd	⊢ ( 𝑅 ∈ Ring → ( 1 · ( 1 ↑ 𝑋 ) ) = 𝑋 )