Metamath Proof Explorer


Theorem resspsradd

Description: A restricted power series algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses resspsr.s
|- S = ( I mPwSer R )
resspsr.h
|- H = ( R |`s T )
resspsr.u
|- U = ( I mPwSer H )
resspsr.b
|- B = ( Base ` U )
resspsr.p
|- P = ( S |`s B )
resspsr.2
|- ( ph -> T e. ( SubRing ` R ) )
Assertion resspsradd
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) )

Proof

Step Hyp Ref Expression
1 resspsr.s
 |-  S = ( I mPwSer R )
2 resspsr.h
 |-  H = ( R |`s T )
3 resspsr.u
 |-  U = ( I mPwSer H )
4 resspsr.b
 |-  B = ( Base ` U )
5 resspsr.p
 |-  P = ( S |`s B )
6 resspsr.2
 |-  ( ph -> T e. ( SubRing ` R ) )
7 eqid
 |-  ( +g ` H ) = ( +g ` H )
8 eqid
 |-  ( +g ` U ) = ( +g ` U )
9 simprl
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X e. B )
10 simprr
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
11 3 4 7 8 9 10 psradd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X oF ( +g ` H ) Y ) )
12 eqid
 |-  ( Base ` S ) = ( Base ` S )
13 eqid
 |-  ( +g ` R ) = ( +g ` R )
14 eqid
 |-  ( +g ` S ) = ( +g ` S )
15 fvex
 |-  ( Base ` R ) e. _V
16 2 subrgbas
 |-  ( T e. ( SubRing ` R ) -> T = ( Base ` H ) )
17 6 16 syl
 |-  ( ph -> T = ( Base ` H ) )
18 eqid
 |-  ( Base ` R ) = ( Base ` R )
19 18 subrgss
 |-  ( T e. ( SubRing ` R ) -> T C_ ( Base ` R ) )
20 6 19 syl
 |-  ( ph -> T C_ ( Base ` R ) )
21 17 20 eqsstrrd
 |-  ( ph -> ( Base ` H ) C_ ( Base ` R ) )
22 mapss
 |-  ( ( ( Base ` R ) e. _V /\ ( Base ` H ) C_ ( Base ` R ) ) -> ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) C_ ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
23 15 21 22 sylancr
 |-  ( ph -> ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) C_ ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
24 23 adantr
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) C_ ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
25 eqid
 |-  ( Base ` H ) = ( Base ` H )
26 eqid
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
27 reldmpsr
 |-  Rel dom mPwSer
28 27 3 4 elbasov
 |-  ( X e. B -> ( I e. _V /\ H e. _V ) )
29 28 ad2antrl
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( I e. _V /\ H e. _V ) )
30 29 simpld
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> I e. _V )
31 3 25 26 4 30 psrbas
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> B = ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
32 1 18 26 12 30 psrbas
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( Base ` S ) = ( ( Base ` R ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
33 24 31 32 3sstr4d
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> B C_ ( Base ` S ) )
34 33 9 sseldd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X e. ( Base ` S ) )
35 33 10 sseldd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y e. ( Base ` S ) )
36 1 12 13 14 34 35 psradd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` S ) Y ) = ( X oF ( +g ` R ) Y ) )
37 2 13 ressplusg
 |-  ( T e. ( SubRing ` R ) -> ( +g ` R ) = ( +g ` H ) )
38 6 37 syl
 |-  ( ph -> ( +g ` R ) = ( +g ` H ) )
39 38 adantr
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( +g ` R ) = ( +g ` H ) )
40 39 ofeqd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> oF ( +g ` R ) = oF ( +g ` H ) )
41 40 oveqd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X oF ( +g ` R ) Y ) = ( X oF ( +g ` H ) Y ) )
42 36 41 eqtrd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` S ) Y ) = ( X oF ( +g ` H ) Y ) )
43 4 fvexi
 |-  B e. _V
44 5 14 ressplusg
 |-  ( B e. _V -> ( +g ` S ) = ( +g ` P ) )
45 43 44 mp1i
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( +g ` S ) = ( +g ` P ) )
46 45 oveqd
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` S ) Y ) = ( X ( +g ` P ) Y ) )
47 11 42 46 3eqtr2d
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) )