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

Metamath Proof Explorer

Theorem psrassa

Description: The ring of power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrcnrg.s 
|- S = ( I mPwSer R )
psrcnrg.i 
|- ( ph -> I e. V )
psrcnrg.r 
|- ( ph -> R e. CRing )
Assertion psrassa 
|- ( ph -> S e. AssAlg )

Proof

Step Hyp Ref Expression
1 psrcnrg.s 
 |-  S = ( I mPwSer R )
2 psrcnrg.i 
 |-  ( ph -> I e. V )
3 psrcnrg.r 
 |-  ( ph -> R e. CRing )
4 eqidd 
 |-  ( ph -> ( Base ` S ) = ( Base ` S ) )
5 1 2 3 psrsca 
 |-  ( ph -> R = ( Scalar ` S ) )
6 eqidd 
 |-  ( ph -> ( Base ` R ) = ( Base ` R ) )
7 eqidd 
 |-  ( ph -> ( .s ` S ) = ( .s ` S ) )
8 eqidd 
 |-  ( ph -> ( .r ` S ) = ( .r ` S ) )
9 3 crngringd 
 |-  ( ph -> R e. Ring )
10 1 2 9 psrlmod 
 |-  ( ph -> S e. LMod )
11 1 2 9 psrring 
 |-  ( ph -> S e. Ring )
12 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> I e. V )
13 9 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Ring )
14 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15 eqid 
 |-  ( .r ` S ) = ( .r ` S )
16 eqid 
 |-  ( Base ` S ) = ( Base ` S )
17 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
18 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
19 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. CRing )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 eqid 
 |-  ( .s ` S ) = ( .s ` S )
22 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` R ) )
23 1 12 13 14 15 16 17 18 19 20 21 22 psrass23 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( ( x ( .s ` S ) y ) ( .r ` S ) z ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) /\ ( y ( .r ` S ) ( x ( .s ` S ) z ) ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) ) )
24 23 simpld 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .s ` S ) y ) ( .r ` S ) z ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) )
25 23 simprd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( .r ` S ) ( x ( .s ` S ) z ) ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) )
26 4 5 6 7 8 10 11 24 25 isassad 
 |-  ( ph -> S e. AssAlg )