Step |
Hyp |
Ref |
Expression |
1 |
|
subrgpsr.s |
|- S = ( I mPwSer R ) |
2 |
|
subrgpsr.h |
|- H = ( R |`s T ) |
3 |
|
subrgpsr.u |
|- U = ( I mPwSer H ) |
4 |
|
subrgpsr.b |
|- B = ( Base ` U ) |
5 |
|
simpl |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> I e. V ) |
6 |
|
subrgrcl |
|- ( T e. ( SubRing ` R ) -> R e. Ring ) |
7 |
6
|
adantl |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> R e. Ring ) |
8 |
1 5 7
|
psrring |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> S e. Ring ) |
9 |
2
|
subrgring |
|- ( T e. ( SubRing ` R ) -> H e. Ring ) |
10 |
9
|
adantl |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> H e. Ring ) |
11 |
3 5 10
|
psrring |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> U e. Ring ) |
12 |
4
|
a1i |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( Base ` U ) ) |
13 |
|
eqid |
|- ( S |`s B ) = ( S |`s B ) |
14 |
|
simpr |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> T e. ( SubRing ` R ) ) |
15 |
1 2 3 4 13 14
|
resspsrbas |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( Base ` ( S |`s B ) ) ) |
16 |
1 2 3 4 13 14
|
resspsradd |
|- ( ( ( I e. V /\ T e. ( SubRing ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` U ) y ) = ( x ( +g ` ( S |`s B ) ) y ) ) |
17 |
1 2 3 4 13 14
|
resspsrmul |
|- ( ( ( I e. V /\ T e. ( SubRing ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` U ) y ) = ( x ( .r ` ( S |`s B ) ) y ) ) |
18 |
12 15 16 17
|
ringpropd |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( U e. Ring <-> ( S |`s B ) e. Ring ) ) |
19 |
11 18
|
mpbid |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( S |`s B ) e. Ring ) |
20 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
21 |
13 20
|
ressbasss |
|- ( Base ` ( S |`s B ) ) C_ ( Base ` S ) |
22 |
15 21
|
eqsstrdi |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B C_ ( Base ` S ) ) |
23 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
24 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
25 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
26 |
|
eqid |
|- ( 1r ` S ) = ( 1r ` S ) |
27 |
1 5 7 23 24 25 26
|
psr1 |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
28 |
25
|
subrg1cl |
|- ( T e. ( SubRing ` R ) -> ( 1r ` R ) e. T ) |
29 |
|
subrgsubg |
|- ( T e. ( SubRing ` R ) -> T e. ( SubGrp ` R ) ) |
30 |
24
|
subg0cl |
|- ( T e. ( SubGrp ` R ) -> ( 0g ` R ) e. T ) |
31 |
29 30
|
syl |
|- ( T e. ( SubRing ` R ) -> ( 0g ` R ) e. T ) |
32 |
28 31
|
ifcld |
|- ( T e. ( SubRing ` R ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. T ) |
33 |
32
|
adantl |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. T ) |
34 |
2
|
subrgbas |
|- ( T e. ( SubRing ` R ) -> T = ( Base ` H ) ) |
35 |
34
|
adantl |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> T = ( Base ` H ) ) |
36 |
33 35
|
eleqtrd |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` H ) ) |
37 |
36
|
adantr |
|- ( ( ( I e. V /\ T e. ( SubRing ` R ) ) /\ x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` H ) ) |
38 |
27 37
|
fmpt3d |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) ) |
39 |
|
fvex |
|- ( Base ` H ) e. _V |
40 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
41 |
40
|
rabex |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V |
42 |
39 41
|
elmap |
|- ( ( 1r ` S ) e. ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> ( 1r ` S ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) ) |
43 |
38 42
|
sylibr |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) e. ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) |
44 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
45 |
3 44 23 4 5
|
psrbas |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B = ( ( Base ` H ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) ) |
46 |
43 45
|
eleqtrrd |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( 1r ` S ) e. B ) |
47 |
22 46
|
jca |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> ( B C_ ( Base ` S ) /\ ( 1r ` S ) e. B ) ) |
48 |
20 26
|
issubrg |
|- ( B e. ( SubRing ` S ) <-> ( ( S e. Ring /\ ( S |`s B ) e. Ring ) /\ ( B C_ ( Base ` S ) /\ ( 1r ` S ) e. B ) ) ) |
49 |
8 19 47 48
|
syl21anbrc |
|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> B e. ( SubRing ` S ) ) |