ply1ass23l

Description: Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	ply1ass23l.p	\|- P = ( Poly1 ` R )
	ply1ass23l.t	\|- .X. = ( .r ` P )
	ply1ass23l.b	\|- B = ( Base ` P )
	ply1ass23l.k	\|- K = ( Base ` R )
	ply1ass23l.n	\|- .x. = ( .s ` P )
Assertion	ply1ass23l	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1ass23l.p	\|- P = ( Poly1 ` R )
2		ply1ass23l.t	\|- .X. = ( .r ` P )
3		ply1ass23l.b	\|- B = ( Base ` P )
4		ply1ass23l.k	\|- K = ( Base ` R )
5		ply1ass23l.n	\|- .x. = ( .s ` P )
6		eqid	\|- ( 1o mPwSer R ) = ( 1o mPwSer R )
7		1on	\|- 1o e. On
8	7	a1i	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> 1o e. On )
9		simpl	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> R e. Ring )
10		eqid	\|- { f e. ( NN0 ^m 1o ) \| ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m 1o ) \| ( `' f " NN ) e. Fin }
11		eqid	\|- ( 1o mPoly R ) = ( 1o mPoly R )
12	1 11 2	ply1mulr	\|- .X. = ( .r ` ( 1o mPoly R ) )
13	11 6 12	mplmulr	\|- .X. = ( .r ` ( 1o mPwSer R ) )
14		eqid	\|- ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) )
15		eqid	\|- ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
16	11 6 15 14	mplbasss	\|- ( Base ` ( 1o mPoly R ) ) C_ ( Base ` ( 1o mPwSer R ) )
17	1 3	ply1bascl2	\|- ( X e. B -> X e. ( Base ` ( 1o mPoly R ) ) )
18	16 17	sseldi	\|- ( X e. B -> X e. ( Base ` ( 1o mPwSer R ) ) )
19	18	3ad2ant2	\|- ( ( A e. K /\ X e. B /\ Y e. B ) -> X e. ( Base ` ( 1o mPwSer R ) ) )
20	19	adantl	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> X e. ( Base ` ( 1o mPwSer R ) ) )
21	1 3	ply1bascl2	\|- ( Y e. B -> Y e. ( Base ` ( 1o mPoly R ) ) )
22	16 21	sseldi	\|- ( Y e. B -> Y e. ( Base ` ( 1o mPwSer R ) ) )
23	22	3ad2ant3	\|- ( ( A e. K /\ X e. B /\ Y e. B ) -> Y e. ( Base ` ( 1o mPwSer R ) ) )
24	23	adantl	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> Y e. ( Base ` ( 1o mPwSer R ) ) )
25	1 11 5	ply1vsca	\|- .x. = ( .s ` ( 1o mPoly R ) )
26	11 6 25	mplvsca2	\|- .x. = ( .s ` ( 1o mPwSer R ) )
27		simpr1	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> A e. K )
28	6 8 9 10 13 14 20 24 4 26 27	psrass23l	\|- ( ( R e. Ring /\ ( A e. K /\ X e. B /\ Y e. B ) ) -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )

Metamath Proof Explorer

Theorem ply1ass23l

Proof