Metamath Proof Explorer

Theorem psrass23l

Description: Associative identity for the ring of power series. Part of psrass23 which does not require the scalar ring to be commutative. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 14-Aug-2019)

Ref Expression
Hypotheses psrring.s 
|- S = ( I mPwSer R )
psrring.i 
|- ( ph -> I e. V )
psrring.r 
|- ( ph -> R e. Ring )
psrass.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrass.t 
|- .X. = ( .r ` S )
psrass.b 
|- B = ( Base ` S )
psrass.x 
|- ( ph -> X e. B )
psrass.y 
|- ( ph -> Y e. B )
psrass23l.k 
|- K = ( Base ` R )
psrass23l.n 
|- .x. = ( .s ` S )
psrass23l.a 
|- ( ph -> A e. K )
Assertion psrass23l 
|- ( ph -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )

Proof

Step Hyp Ref Expression
1 psrring.s 
 |-  S = ( I mPwSer R )
2 psrring.i 
 |-  ( ph -> I e. V )
3 psrring.r 
 |-  ( ph -> R e. Ring )
4 psrass.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psrass.t 
 |-  .X. = ( .r ` S )
6 psrass.b 
 |-  B = ( Base ` S )
7 psrass.x 
 |-  ( ph -> X e. B )
8 psrass.y 
 |-  ( ph -> Y e. B )
9 psrass23l.k 
 |-  K = ( Base ` R )
10 psrass23l.n 
 |-  .x. = ( .s ` S )
11 psrass23l.a 
 |-  ( ph -> A e. K )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 11 adantr 
 |-  ( ( ph /\ k e. D ) -> A e. K )
15 14 9 eleqtrdi 
 |-  ( ( ph /\ k e. D ) -> A e. ( Base ` R ) )
16 15 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> A e. ( Base ` R ) )
17 7 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X e. B )
18 ssrab2 
 |-  { y e. D | y oR <_ k } C_ D
19 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } )
20 18 19 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
21 1 10 12 6 13 4 16 17 20 psrvscaval 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( A .x. X ) ` x ) = ( A ( .r ` R ) ( X ` x ) ) )
22 21 oveq1d 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) = ( ( A ( .r ` R ) ( X ` x ) ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) )
23 3 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
24 1 12 4 6 17 psrelbas 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
25 24 20 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
26 8 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y e. B )
27 1 12 4 6 26 psrelbas 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
28 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D )
29 eqid 
 |-  { y e. D | y oR <_ k } = { y e. D | y oR <_ k }
30 4 29 psrbagconcl 
 |-  ( ( k e. D /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
31 28 19 30 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
32 18 31 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
33 27 32 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
34 12 13 ringass 
 |-  ( ( R e. Ring /\ ( A e. ( Base ` R ) /\ ( X ` x ) e. ( Base ` R ) /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) ) -> ( ( A ( .r ` R ) ( X ` x ) ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) = ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) )
35 23 16 25 33 34 syl13anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( A ( .r ` R ) ( X ` x ) ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) = ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) )
36 22 35 eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) = ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) )
37 36 mpteq2dva 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) )
38 37 oveq2d 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) = ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
39 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
40 eqid 
 |-  ( +g ` R ) = ( +g ` R )
41 3 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
42 4 psrbaglefi 
 |-  ( k e. D -> { y e. D | y oR <_ k } e. Fin )
43 42 adantl 
 |-  ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
44 12 13 ringcl 
 |-  ( ( R e. Ring /\ ( X ` x ) e. ( Base ` R ) /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
45 23 25 33 44 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
46 ovex 
 |-  ( NN0 ^m I ) e. _V
47 4 46 rabex2 
 |-  D e. _V
48 47 mptrabex 
 |-  ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) e. _V
49 funmpt 
 |-  Fun ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) )
50 fvex 
 |-  ( 0g ` R ) e. _V
51 48 49 50 3pm3.2i 
 |-  ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) e. _V /\ Fun ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) /\ ( 0g ` R ) e. _V )
52 51 a1i 
 |-  ( ( ph /\ k e. D ) -> ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) e. _V /\ Fun ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) /\ ( 0g ` R ) e. _V ) )
53 suppssdm 
 |-  ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) supp ( 0g ` R ) ) C_ dom ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) )
54 eqid 
 |-  ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) )
55 54 dmmptss 
 |-  dom ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) C_ { y e. D | y oR <_ k }
56 53 55 sstri 
 |-  ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) supp ( 0g ` R ) ) C_ { y e. D | y oR <_ k }
57 56 a1i 
 |-  ( ( ph /\ k e. D ) -> ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) supp ( 0g ` R ) ) C_ { y e. D | y oR <_ k } )
58 suppssfifsupp 
 |-  ( ( ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) e. _V /\ Fun ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { y e. D | y oR <_ k } e. Fin /\ ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) supp ( 0g ` R ) ) C_ { y e. D | y oR <_ k } ) ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )
59 52 43 57 58 syl12anc 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )
60 12 39 40 13 41 43 15 45 59 gsummulc2 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) = ( A ( .r ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
61 38 60 eqtrd 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) = ( A ( .r ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
62 61 mpteq2dva 
 |-  ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) = ( k e. D |-> ( A ( .r ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) ) )
63 1 10 9 6 3 11 7 psrvscacl 
 |-  ( ph -> ( A .x. X ) e. B )
64 1 6 13 5 4 63 8 psrmulfval 
 |-  ( ph -> ( ( A .x. X ) .X. Y ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( ( A .x. X ) ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
65 1 6 5 3 7 8 psrmulcl 
 |-  ( ph -> ( X .X. Y ) e. B )
66 1 10 9 6 13 4 11 65 psrvsca 
 |-  ( ph -> ( A .x. ( X .X. Y ) ) = ( ( D X. { A } ) oF ( .r ` R ) ( X .X. Y ) ) )
67 47 a1i 
 |-  ( ph -> D e. _V )
68 ovexd 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. _V )
69 fconstmpt 
 |-  ( D X. { A } ) = ( k e. D |-> A )
70 69 a1i 
 |-  ( ph -> ( D X. { A } ) = ( k e. D |-> A ) )
71 1 6 13 5 4 7 8 psrmulfval 
 |-  ( ph -> ( X .X. Y ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) )
72 67 14 68 70 71 offval2 
 |-  ( ph -> ( ( D X. { A } ) oF ( .r ` R ) ( X .X. Y ) ) = ( k e. D |-> ( A ( .r ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) ) )
73 66 72 eqtrd 
 |-  ( ph -> ( A .x. ( X .X. Y ) ) = ( k e. D |-> ( A ( .r ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ) ) )
74 62 64 73 3eqtr4d 
 |-  ( ph -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )