Metamath Proof Explorer

Theorem psrass23

Description: Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 25-Nov-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 )
psrcom.c 
|- ( ph -> R e. CRing )
psrass.k 
|- K = ( Base ` R )
psrass.n 
|- .x. = ( .s ` S )
psrass.a 
|- ( ph -> A e. K )
Assertion psrass23 
|- ( ph -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .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 psrcom.c 
 |-  ( ph -> R e. CRing )
10 psrass.k 
 |-  K = ( Base ` R )
11 psrass.n 
 |-  .x. = ( .s ` S )
12 psrass.a 
 |-  ( ph -> A e. K )
13 1 2 3 4 5 6 7 8 10 11 12 psrass23l 
 |-  ( ph -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 12 adantr 
 |-  ( ( ph /\ k e. D ) -> A e. K )
17 16 10 eleqtrdi 
 |-  ( ( ph /\ k e. D ) -> A e. ( Base ` R ) )
18 17 adantr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> A e. ( Base ` R ) )
19 8 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y e. B )
20 ssrab2 
 |-  { y e. D | y oR <_ k } C_ D
21 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D )
22 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } )
23 eqid 
 |-  { y e. D | y oR <_ k } = { y e. D | y oR <_ k }
24 4 23 psrbagconcl 
 |-  ( ( k e. D /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
25 21 22 24 syl2anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
26 20 25 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
27 1 11 14 6 15 4 18 19 26 psrvscaval 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( A .x. Y ) ` ( k oF - x ) ) = ( A ( .r ` R ) ( Y ` ( k oF - x ) ) ) )
28 27 oveq2d 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( A .x. Y ) ` ( k oF - x ) ) ) = ( ( X ` x ) ( .r ` R ) ( A ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) )
29 7 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X e. B )
30 1 14 4 6 29 psrelbas 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
31 20 22 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
32 30 31 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
33 1 14 4 6 19 psrelbas 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
34 33 26 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
35 9 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. CRing )
36 14 15 crngcom 
 |-  ( ( R e. CRing /\ u e. ( Base ` R ) /\ v e. ( Base ` R ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) )
37 36 3expb 
 |-  ( ( R e. CRing /\ ( u e. ( Base ` R ) /\ v e. ( Base ` R ) ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) )
38 35 37 sylan 
 |-  ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( u e. ( Base ` R ) /\ v e. ( Base ` R ) ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) )
39 3 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
40 14 15 ringass 
 |-  ( ( R e. Ring /\ ( u e. ( Base ` R ) /\ v e. ( Base ` R ) /\ w e. ( Base ` R ) ) ) -> ( ( u ( .r ` R ) v ) ( .r ` R ) w ) = ( u ( .r ` R ) ( v ( .r ` R ) w ) ) )
41 39 40 sylan 
 |-  ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( u e. ( Base ` R ) /\ v e. ( Base ` R ) /\ w e. ( Base ` R ) ) ) -> ( ( u ( .r ` R ) v ) ( .r ` R ) w ) = ( u ( .r ` R ) ( v ( .r ` R ) w ) ) )
42 32 18 34 38 41 caov12d 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( A ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) = ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) )
43 28 42 eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( A .x. Y ) ` ( k oF - x ) ) ) = ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) )
44 43 mpteq2dva 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( A .x. Y ) ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( A ( .r ` R ) ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) )
45 44 oveq2d 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( A .x. 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 ) ) ) ) ) ) )
46 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
47 eqid 
 |-  ( +g ` R ) = ( +g ` R )
48 3 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
49 4 psrbaglefi 
 |-  ( k e. D -> { y e. D | y oR <_ k } e. Fin )
50 49 adantl 
 |-  ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
51 14 15 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 ) )
52 39 32 34 51 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
53 ovex 
 |-  ( NN0 ^m I ) e. _V
54 4 53 rabex2 
 |-  D e. _V
55 54 mptrabex 
 |-  ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) e. _V
56 funmpt 
 |-  Fun ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) )
57 fvex 
 |-  ( 0g ` R ) e. _V
58 55 56 57 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 )
59 58 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 ) )
60 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 ) ) ) )
61 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 ) ) ) )
62 61 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 }
63 60 62 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 }
64 63 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 } )
65 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 ) )
66 59 50 64 65 syl12anc 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) finSupp ( 0g ` R ) )
67 14 46 47 15 48 50 17 52 66 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 ) ) ) ) ) ) )
68 45 67 eqtrd 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( A .x. 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 ) ) ) ) ) ) )
69 68 mpteq2dva 
 |-  ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( A .x. 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 ) ) ) ) ) ) ) )
70 1 11 10 6 3 12 8 psrvscacl 
 |-  ( ph -> ( A .x. Y ) e. B )
71 1 6 15 5 4 7 70 psrmulfval 
 |-  ( ph -> ( X .X. ( A .x. Y ) ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( A .x. Y ) ` ( k oF - x ) ) ) ) ) ) )
72 1 6 5 3 7 8 psrmulcl 
 |-  ( ph -> ( X .X. Y ) e. B )
73 1 11 10 6 15 4 12 72 psrvsca 
 |-  ( ph -> ( A .x. ( X .X. Y ) ) = ( ( D X. { A } ) oF ( .r ` R ) ( X .X. Y ) ) )
74 54 a1i 
 |-  ( ph -> D e. _V )
75 ovex 
 |-  ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. _V
76 75 a1i 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) e. _V )
77 fconstmpt 
 |-  ( D X. { A } ) = ( k e. D |-> A )
78 77 a1i 
 |-  ( ph -> ( D X. { A } ) = ( k e. D |-> A ) )
79 1 6 15 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 ) ) ) ) ) ) )
80 74 16 76 78 79 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 ) ) ) ) ) ) ) )
81 73 80 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 ) ) ) ) ) ) ) )
82 69 71 81 3eqtr4d 
 |-  ( ph -> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) )
83 13 82 jca 
 |-  ( ph -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )