Metamath Proof Explorer

Theorem psrgrpOLD

Description: Obsolete version of psrgrp as of 7-Feb-2025. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses psrgrp.s 
|- S = ( I mPwSer R )
psrgrp.i 
|- ( ph -> I e. V )
psrgrp.r 
|- ( ph -> R e. Grp )
Assertion psrgrpOLD 
|- ( ph -> S e. Grp )

Proof

Step Hyp Ref Expression
1 psrgrp.s 
 |-  S = ( I mPwSer R )
2 psrgrp.i 
 |-  ( ph -> I e. V )
3 psrgrp.r 
 |-  ( ph -> R e. Grp )
4 eqidd 
 |-  ( ph -> ( Base ` S ) = ( Base ` S ) )
5 eqidd 
 |-  ( ph -> ( +g ` S ) = ( +g ` S ) )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( +g ` S ) = ( +g ` S )
8 3 grpmgmd 
 |-  ( ph -> R e. Mgm )
9 8 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. Mgm )
10 simp2 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) )
11 simp3 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
12 1 6 7 9 10 11 psraddcl 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 13 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
15 14 a1i 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
18 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` S ) )
19 1 16 17 6 18 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
20 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
21 1 16 17 6 20 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
22 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
23 1 16 17 6 22 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
24 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Grp )
25 eqid 
 |-  ( +g ` R ) = ( +g ` R )
26 16 25 grpass 
 |-  ( ( R e. Grp /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( +g ` R ) s ) ( +g ` R ) t ) = ( r ( +g ` R ) ( s ( +g ` R ) t ) ) )
27 24 26 sylan 
 |-  ( ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( +g ` R ) s ) ( +g ` R ) t ) = ( r ( +g ` R ) ( s ( +g ` R ) t ) ) )
28 15 19 21 23 27 caofass 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x oF ( +g ` R ) y ) oF ( +g ` R ) z ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
29 1 6 25 7 18 20 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) = ( x oF ( +g ` R ) y ) )
30 29 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) oF ( +g ` R ) z ) = ( ( x oF ( +g ` R ) y ) oF ( +g ` R ) z ) )
31 1 6 25 7 20 22 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) = ( y oF ( +g ` R ) z ) )
32 31 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x oF ( +g ` R ) ( y ( +g ` S ) z ) ) = ( x oF ( +g ` R ) ( y oF ( +g ` R ) z ) ) )
33 28 30 32 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) oF ( +g ` R ) z ) = ( x oF ( +g ` R ) ( y ( +g ` S ) z ) ) )
34 12 3adant3r3 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
35 1 6 25 7 34 22 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) ( +g ` S ) z ) = ( ( x ( +g ` S ) y ) oF ( +g ` R ) z ) )
36 8 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Mgm )
37 1 6 7 36 20 22 psraddcl 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) e. ( Base ` S ) )
38 1 6 25 7 18 37 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` S ) ( y ( +g ` S ) z ) ) = ( x oF ( +g ` R ) ( y ( +g ` S ) z ) ) )
39 33 35 38 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) ( +g ` S ) z ) = ( x ( +g ` S ) ( y ( +g ` S ) z ) ) )
40 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
41 1 2 3 17 40 6 psr0cl 
 |-  ( ph -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) e. ( Base ` S ) )
42 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> I e. V )
43 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> R e. Grp )
44 simpr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) )
45 1 42 43 17 40 6 7 44 psr0lid 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) ( +g ` S ) x ) = x )
46 eqid 
 |-  ( invg ` R ) = ( invg ` R )
47 1 42 43 17 46 6 44 psrnegcl 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( invg ` R ) o. x ) e. ( Base ` S ) )
48 1 42 43 17 46 6 44 40 7 psrlinv 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( ( invg ` R ) o. x ) ( +g ` S ) x ) = ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) )
49 4 5 12 39 41 45 47 48 isgrpd 
 |-  ( ph -> S e. Grp )