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

Metamath Proof Explorer

Theorem 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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 ) ) )