Metamath Proof Explorer

Theorem psrdi

Description: Distributive law for the ring of power series (left-distributivity). (Contributed by Mario Carneiro, 7-Jan-2015)

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 )
psrass.z 
|- ( ph -> Z e. B )
psrdi.a 
|- .+ = ( +g ` S )
Assertion psrdi 
|- ( ph -> ( X .X. ( Y .+ Z ) ) = ( ( X .X. Y ) .+ ( X .X. Z ) ) )

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 psrass.z 
 |-  ( ph -> Z e. B )
10 psrdi.a 
 |-  .+ = ( +g ` S )
11 eqid 
 |-  ( +g ` R ) = ( +g ` R )
12 1 6 11 10 8 9 psradd 
 |-  ( ph -> ( Y .+ Z ) = ( Y oF ( +g ` R ) Z ) )
13 12 fveq1d 
 |-  ( ph -> ( ( Y .+ Z ) ` ( k oF - x ) ) = ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) )
14 13 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y .+ Z ) ` ( k oF - x ) ) = ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) )
15 ssrab2 
 |-  { y e. D | y oR <_ k } C_ D
16 2 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> I e. V )
17 simplr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> k e. D )
18 simpr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } )
19 eqid 
 |-  { y e. D | y oR <_ k } = { y e. D | y oR <_ k }
20 4 19 psrbagconcl 
 |-  ( ( I e. V /\ k e. D /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
21 16 17 18 20 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
22 15 21 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 1 23 4 6 8 psrelbas 
 |-  ( ph -> Y : D --> ( Base ` R ) )
25 24 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
26 25 ffnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y Fn D )
27 1 23 4 6 9 psrelbas 
 |-  ( ph -> Z : D --> ( Base ` R ) )
28 27 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Z : D --> ( Base ` R ) )
29 28 ffnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Z Fn D )
30 ovex 
 |-  ( NN0 ^m I ) e. _V
31 4 30 rabex2 
 |-  D e. _V
32 31 a1i 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> D e. _V )
33 inidm 
 |-  ( D i^i D ) = D
34 eqidd 
 |-  ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. D ) -> ( Y ` ( k oF - x ) ) = ( Y ` ( k oF - x ) ) )
35 eqidd 
 |-  ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. D ) -> ( Z ` ( k oF - x ) ) = ( Z ` ( k oF - x ) ) )
36 26 29 32 32 33 34 35 ofval 
 |-  ( ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) /\ ( k oF - x ) e. D ) -> ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) = ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) )
37 22 36 mpdan 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y oF ( +g ` R ) Z ) ` ( k oF - x ) ) = ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) )
38 14 37 eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( Y .+ Z ) ` ( k oF - x ) ) = ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) )
39 38 oveq2d 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) = ( ( X ` x ) ( .r ` R ) ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) )
40 3 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
41 1 23 4 6 7 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
43 15 18 sseldi 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
44 42 43 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
45 25 22 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
46 28 22 ffvelrnd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Z ` ( k oF - x ) ) e. ( Base ` R ) )
47 eqid 
 |-  ( .r ` R ) = ( .r ` R )
48 23 11 47 ringdi 
 |-  ( ( R e. Ring /\ ( ( X ` x ) e. ( Base ` R ) /\ ( Y ` ( k oF - x ) ) e. ( Base ` R ) /\ ( Z ` ( k oF - x ) ) e. ( Base ` R ) ) ) -> ( ( X ` x ) ( .r ` R ) ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) = ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) )
49 40 44 45 46 48 syl13anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( Y ` ( k oF - x ) ) ( +g ` R ) ( Z ` ( k oF - x ) ) ) ) = ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) )
50 39 49 eqtrd 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) = ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) )
51 50 mpteq2dva 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) )
52 4 psrbaglefi 
 |-  ( ( I e. V /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
53 2 52 sylan 
 |-  ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
54 23 47 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 ) )
55 40 44 45 54 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
56 23 47 ringcl 
 |-  ( ( R e. Ring /\ ( X ` x ) e. ( Base ` R ) /\ ( Z ` ( k oF - x ) ) e. ( Base ` R ) ) -> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) e. ( Base ` R ) )
57 40 44 46 56 syl3anc 
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) e. ( Base ` R ) )
58 eqidd 
 |-  ( ( ph /\ k e. D ) -> ( 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 ) ) ) ) )
59 eqidd 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) )
60 53 55 57 58 59 offval2 
 |-  ( ( ph /\ k e. D ) -> ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ( +g ` R ) ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) )
61 51 60 eqtr4d 
 |-  ( ( ph /\ k e. D ) -> ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) = ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) )
62 61 oveq2d 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) = ( R gsum ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) )
63 3 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
64 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
65 63 64 syl 
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
66 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 ) ) ) )
67 eqid 
 |-  ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) )
68 23 11 65 53 55 57 66 67 gsummptfidmadd2 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) oF ( +g ` R ) ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) = ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) )
69 62 68 eqtrd 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) = ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) )
70 69 mpteq2dva 
 |-  ( ph -> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) ) = ( k e. D |-> ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) )
71 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
72 3 71 syl 
 |-  ( ph -> R e. Grp )
73 1 6 10 72 8 9 psraddcl 
 |-  ( ph -> ( Y .+ Z ) e. B )
74 1 6 47 5 4 7 73 psrmulfval 
 |-  ( ph -> ( X .X. ( Y .+ Z ) ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( ( Y .+ Z ) ` ( k oF - x ) ) ) ) ) ) )
75 1 6 5 3 7 8 psrmulcl 
 |-  ( ph -> ( X .X. Y ) e. B )
76 1 6 5 3 7 9 psrmulcl 
 |-  ( ph -> ( X .X. Z ) e. B )
77 1 6 11 10 75 76 psradd 
 |-  ( ph -> ( ( X .X. Y ) .+ ( X .X. Z ) ) = ( ( X .X. Y ) oF ( +g ` R ) ( X .X. Z ) ) )
78 31 a1i 
 |-  ( ph -> D e. _V )
79 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 )
80 ovexd 
 |-  ( ( ph /\ k e. D ) -> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) e. _V )
81 1 6 47 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 ) ) ) ) ) ) )
82 1 6 47 5 4 7 9 psrmulfval 
 |-  ( ph -> ( X .X. Z ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) )
83 78 79 80 81 82 offval2 
 |-  ( ph -> ( ( X .X. Y ) oF ( +g ` R ) ( X .X. Z ) ) = ( k e. D |-> ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) )
84 77 83 eqtrd 
 |-  ( ph -> ( ( X .X. Y ) .+ ( X .X. Z ) ) = ( k e. D |-> ( ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) ) ) ) ) )
85 70 74 84 3eqtr4d 
 |-  ( ph -> ( X .X. ( Y .+ Z ) ) = ( ( X .X. Y ) .+ ( X .X. Z ) ) )