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 |
|
eqidd |
|- ( ph -> ( Base ` S ) = ( Base ` S ) ) |
5 |
|
eqidd |
|- ( ph -> ( +g ` S ) = ( +g ` S ) ) |
6 |
|
eqidd |
|- ( ph -> ( .r ` S ) = ( .r ` S ) ) |
7 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
8 |
3 7
|
syl |
|- ( ph -> R e. Grp ) |
9 |
1 2 8
|
psrgrp |
|- ( ph -> S e. Grp ) |
10 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
11 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
12 |
3
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. Ring ) |
13 |
|
simp2 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) ) |
14 |
|
simp3 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) ) |
15 |
1 10 11 12 13 14
|
psrmulcl |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( .r ` S ) y ) e. ( Base ` S ) ) |
16 |
2
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> I e. V ) |
17 |
3
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Ring ) |
18 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
19 |
|
simpr1 |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` S ) ) |
20 |
|
simpr2 |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) ) |
21 |
|
simpr3 |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) ) |
22 |
1 16 17 18 11 10 19 20 21
|
psrass1 |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .r ` S ) y ) ( .r ` S ) z ) = ( x ( .r ` S ) ( y ( .r ` S ) z ) ) ) |
23 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
24 |
1 16 17 18 11 10 19 20 21 23
|
psrdi |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .r ` S ) ( y ( +g ` S ) z ) ) = ( ( x ( .r ` S ) y ) ( +g ` S ) ( x ( .r ` S ) z ) ) ) |
25 |
1 16 17 18 11 10 19 20 21 23
|
psrdir |
|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) ( .r ` S ) z ) = ( ( x ( .r ` S ) z ) ( +g ` S ) ( y ( .r ` S ) z ) ) ) |
26 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
27 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
28 |
|
eqid |
|- ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) |
29 |
1 2 3 18 26 27 28 10
|
psr1cl |
|- ( ph -> ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( Base ` S ) ) |
30 |
2
|
adantr |
|- ( ( ph /\ x e. ( Base ` S ) ) -> I e. V ) |
31 |
3
|
adantr |
|- ( ( ph /\ x e. ( Base ` S ) ) -> R e. Ring ) |
32 |
|
simpr |
|- ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) ) |
33 |
1 30 31 18 26 27 28 10 11 32
|
psrlidm |
|- ( ( ph /\ x e. ( Base ` S ) ) -> ( ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` S ) x ) = x ) |
34 |
1 30 31 18 26 27 28 10 11 32
|
psrridm |
|- ( ( ph /\ x e. ( Base ` S ) ) -> ( x ( .r ` S ) ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = x ) |
35 |
4 5 6 9 15 22 24 25 29 33 34
|
isringd |
|- ( ph -> S e. Ring ) |