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 eqid
 |-  { y e. D | y oR <_ k } = { y e. D | y oR <_ k }
17 4 16 psrbagconcl
 |-  ( ( k e. D /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
18 17 adantll
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. { y e. D | y oR <_ k } )
19 15 18 sselid
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( k oF - x ) e. D )
20 eqid
 |-  ( Base ` R ) = ( Base ` R )
21 1 20 4 6 8 psrelbas
 |-  ( ph -> Y : D --> ( Base ` R ) )
22 21 ad2antrr
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y : D --> ( Base ` R ) )
23 22 ffnd
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Y Fn D )
24 1 20 4 6 9 psrelbas
 |-  ( ph -> Z : D --> ( Base ` R ) )
25 24 ad2antrr
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Z : D --> ( Base ` R ) )
26 25 ffnd
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> Z Fn D )
27 ovex
 |-  ( NN0 ^m I ) e. _V
28 4 27 rabex2
 |-  D e. _V
29 28 a1i
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> D e. _V )
30 inidm
 |-  ( D i^i D ) = D
31 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 ) ) )
32 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 ) ) )
33 23 26 29 29 30 31 32 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 ) ) ) )
34 19 33 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 ) ) ) )
35 14 34 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 ) ) ) )
36 35 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 ) ) ) ) )
37 3 ad2antrr
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> R e. Ring )
38 1 20 4 6 7 psrelbas
 |-  ( ph -> X : D --> ( Base ` R ) )
39 38 ad2antrr
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> X : D --> ( Base ` R ) )
40 simpr
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. { y e. D | y oR <_ k } )
41 15 40 sselid
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> x e. D )
42 39 41 ffvelcdmd
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( X ` x ) e. ( Base ` R ) )
43 22 19 ffvelcdmd
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Y ` ( k oF - x ) ) e. ( Base ` R ) )
44 25 19 ffvelcdmd
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( Z ` ( k oF - x ) ) e. ( Base ` R ) )
45 eqid
 |-  ( .r ` R ) = ( .r ` R )
46 20 11 45 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 ) ) ) ) )
47 37 42 43 44 46 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 ) ) ) ) )
48 36 47 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 ) ) ) ) )
49 48 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 ) ) ) ) ) )
50 4 psrbaglefi
 |-  ( k e. D -> { y e. D | y oR <_ k } e. Fin )
51 50 adantl
 |-  ( ( ph /\ k e. D ) -> { y e. D | y oR <_ k } e. Fin )
52 20 45 37 42 43 ringcld
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Y ` ( k oF - x ) ) ) e. ( Base ` R ) )
53 20 45 37 42 44 ringcld
 |-  ( ( ( ph /\ k e. D ) /\ x e. { y e. D | y oR <_ k } ) -> ( ( X ` x ) ( .r ` R ) ( Z ` ( k oF - x ) ) ) e. ( Base ` R ) )
54 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 ) ) ) ) )
55 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 ) ) ) ) )
56 51 52 53 54 55 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 ) ) ) ) ) )
57 49 56 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 ) ) ) ) ) )
58 57 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 ) ) ) ) ) ) )
59 3 adantr
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
60 59 ringcmnd
 |-  ( ( ph /\ k e. D ) -> R e. CMnd )
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 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 ) ) ) )
63 20 11 60 51 52 53 61 62 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 ) ) ) ) ) ) )
64 58 63 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 ) ) ) ) ) ) )
65 64 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 ) ) ) ) ) ) ) )
66 3 ringgrpd
 |-  ( ph -> R e. Grp )
67 66 grpmgmd
 |-  ( ph -> R e. Mgm )
68 1 6 10 67 8 9 psraddcl
 |-  ( ph -> ( Y .+ Z ) e. B )
69 1 6 45 5 4 7 68 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 ) ) ) ) ) ) )
70 1 6 5 3 7 8 psrmulcl
 |-  ( ph -> ( X .X. Y ) e. B )
71 1 6 5 3 7 9 psrmulcl
 |-  ( ph -> ( X .X. Z ) e. B )
72 1 6 11 10 70 71 psradd
 |-  ( ph -> ( ( X .X. Y ) .+ ( X .X. Z ) ) = ( ( X .X. Y ) oF ( +g ` R ) ( X .X. Z ) ) )
73 28 a1i
 |-  ( ph -> D e. _V )
74 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 )
75 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 )
76 1 6 45 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 ) ) ) ) ) ) )
77 1 6 45 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 ) ) ) ) ) ) )
78 73 74 75 76 77 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 ) ) ) ) ) ) ) )
79 72 78 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 ) ) ) ) ) ) ) )
80 65 69 79 3eqtr4d
 |-  ( ph -> ( X .X. ( Y .+ Z ) ) = ( ( X .X. Y ) .+ ( X .X. Z ) ) )