Metamath Proof Explorer

Theorem grpidpropd

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014)

Ref Expression
Hypotheses grpidpropd.1 
|- ( ph -> B = ( Base ` K ) )
grpidpropd.2 
|- ( ph -> B = ( Base ` L ) )
grpidpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
Assertion grpidpropd 
|- ( ph -> ( 0g ` K ) = ( 0g ` L ) )

Proof

Step Hyp Ref Expression
1 grpidpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 grpidpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 grpidpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 3 eqeq1d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x ( +g ` K ) y ) = y <-> ( x ( +g ` L ) y ) = y ) )
5 3 oveqrspc2v 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( +g ` K ) w ) = ( z ( +g ` L ) w ) )
6 5 oveqrspc2v 
 |-  ( ( ph /\ ( y e. B /\ x e. B ) ) -> ( y ( +g ` K ) x ) = ( y ( +g ` L ) x ) )
7 6 ancom2s 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y ( +g ` K ) x ) = ( y ( +g ` L ) x ) )
8 7 eqeq1d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( y ( +g ` K ) x ) = y <-> ( y ( +g ` L ) x ) = y ) )
9 4 8 anbi12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) <-> ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) )
10 9 anassrs 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) <-> ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) )
11 10 ralbidva 
 |-  ( ( ph /\ x e. B ) -> ( A. y e. B ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) <-> A. y e. B ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) )
12 11 pm5.32da 
 |-  ( ph -> ( ( x e. B /\ A. y e. B ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) <-> ( x e. B /\ A. y e. B ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) ) )
13 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` K ) ) )
14 1 raleqdv 
 |-  ( ph -> ( A. y e. B ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) <-> A. y e. ( Base ` K ) ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) )
15 13 14 anbi12d 
 |-  ( ph -> ( ( x e. B /\ A. y e. B ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) <-> ( x e. ( Base ` K ) /\ A. y e. ( Base ` K ) ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) ) )
16 2 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` L ) ) )
17 2 raleqdv 
 |-  ( ph -> ( A. y e. B ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) <-> A. y e. ( Base ` L ) ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) )
18 16 17 anbi12d 
 |-  ( ph -> ( ( x e. B /\ A. y e. B ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) <-> ( x e. ( Base ` L ) /\ A. y e. ( Base ` L ) ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) ) )
19 12 15 18 3bitr3d 
 |-  ( ph -> ( ( x e. ( Base ` K ) /\ A. y e. ( Base ` K ) ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) <-> ( x e. ( Base ` L ) /\ A. y e. ( Base ` L ) ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) ) )
20 19 iotabidv 
 |-  ( ph -> ( iota x ( x e. ( Base ` K ) /\ A. y e. ( Base ` K ) ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) ) = ( iota x ( x e. ( Base ` L ) /\ A. y e. ( Base ` L ) ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) ) )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 eqid 
 |-  ( +g ` K ) = ( +g ` K )
23 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
24 21 22 23 grpidval 
 |-  ( 0g ` K ) = ( iota x ( x e. ( Base ` K ) /\ A. y e. ( Base ` K ) ( ( x ( +g ` K ) y ) = y /\ ( y ( +g ` K ) x ) = y ) ) )
25 eqid 
 |-  ( Base ` L ) = ( Base ` L )
26 eqid 
 |-  ( +g ` L ) = ( +g ` L )
27 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
28 25 26 27 grpidval 
 |-  ( 0g ` L ) = ( iota x ( x e. ( Base ` L ) /\ A. y e. ( Base ` L ) ( ( x ( +g ` L ) y ) = y /\ ( y ( +g ` L ) x ) = y ) ) )
29 20 24 28 3eqtr4g 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )