Theorem ply1vr1smo

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

	Ref	Expression
Hypotheses	ply1vr1smo.p	|- P = ( Poly1 ` R )
	ply1vr1smo.i	|- .1. = ( 1r ` R )
	ply1vr1smo.t	|- .x. = ( .s ` P )
	ply1vr1smo.m	|- G = ( mulGrp ` P )
	ply1vr1smo.e	|- .^ = ( .g ` G )
	ply1vr1smo.x	|- X = ( var1 ` R )
Assertion	ply1vr1smo	|- ( R e. Ring -> ( .1. .x. ( 1 .^ X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		ply1vr1smo.p	|- P = ( Poly1 ` R )
2		ply1vr1smo.i	|- .1. = ( 1r ` R )
3		ply1vr1smo.t	|- .x. = ( .s ` P )
4		ply1vr1smo.m	|- G = ( mulGrp ` P )
5		ply1vr1smo.e	|- .^ = ( .g ` G )
6		ply1vr1smo.x	|- X = ( var1 ` R )
7	1	ply1sca	|- ( R e. Ring -> R = ( Scalar ` P ) )
8	7	fveq2d	|- ( R e. Ring -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
9	2 8	syl5eq	|- ( R e. Ring -> .1. = ( 1r ` ( Scalar ` P ) ) )
10	9	oveq1d	|- ( R e. Ring -> ( .1. .x. ( 1 .^ X ) ) = ( ( 1r ` ( Scalar ` P ) ) .x. ( 1 .^ X ) ) )
11	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
12		eqid	|- ( Base ` P ) = ( Base ` P )
13	6 1 12	vr1cl	|- ( R e. Ring -> X e. ( Base ` P ) )
14	4 12	mgpbas	|- ( Base ` P ) = ( Base ` G )
15	14 5	mulg1	|- ( X e. ( Base ` P ) -> ( 1 .^ X ) = X )
16	13 15	syl	|- ( R e. Ring -> ( 1 .^ X ) = X )
17	16 13	eqeltrd	|- ( R e. Ring -> ( 1 .^ X ) e. ( Base ` P ) )
18		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
19		eqid	|- ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
20	12 18 3 19	lmodvs1	|- ( ( P e. LMod /\ ( 1 .^ X ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) .x. ( 1 .^ X ) ) = ( 1 .^ X ) )
21	11 17 20	syl2anc	|- ( R e. Ring -> ( ( 1r ` ( Scalar ` P ) ) .x. ( 1 .^ X ) ) = ( 1 .^ X ) )
22	10 21 16	3eqtrd	|- ( R e. Ring -> ( .1. .x. ( 1 .^ X ) ) = X )