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 ofeq 
 |-  ( ( +g ` R ) = ( +g ` H ) -> oF ( +g ` R ) = oF ( +g ` H ) )
41 39 40 syl 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> oF ( +g ` R ) = oF ( +g ` H ) )
42 41 oveqd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X oF ( +g ` R ) Y ) = ( X oF ( +g ` H ) Y ) )
43 36 42 eqtrd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` S ) Y ) = ( X oF ( +g ` H ) Y ) )
44 4 fvexi 
 |-  B e. _V
45 5 14 ressplusg 
 |-  ( B e. _V -> ( +g ` S ) = ( +g ` P ) )
46 44 45 mp1i 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( +g ` S ) = ( +g ` P ) )
47 46 oveqd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` S ) Y ) = ( X ( +g ` P ) Y ) )
48 11 43 47 3eqtr2d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X ( +g ` U ) Y ) = ( X ( +g ` P ) Y ) )