Metamath Proof Explorer

Theorem urpropd

Description: Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses urpropd.b 
|- B = ( Base ` S )
urpropd.s 
|- ( ph -> S e. V )
urpropd.t 
|- ( ph -> T e. W )
urpropd.1 
|- ( ph -> B = ( Base ` T ) )
urpropd.2 
|- ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) )
Assertion urpropd 
|- ( ph -> ( 1r ` S ) = ( 1r ` T ) )

Proof

Step Hyp Ref Expression
1 urpropd.b 
 |-  B = ( Base ` S )
2 urpropd.s 
 |-  ( ph -> S e. V )
3 urpropd.t 
 |-  ( ph -> T e. W )
4 urpropd.1 
 |-  ( ph -> B = ( Base ` T ) )
5 urpropd.2 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) )
6 4 adantr 
 |-  ( ( ph /\ e e. B ) -> B = ( Base ` T ) )
7 5 anasss 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) )
8 7 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) )
9 8 ad2antrr 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> A. x e. B A. y e. B ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) )
10 oveq1 
 |-  ( x = e -> ( x ( .r ` S ) y ) = ( e ( .r ` S ) y ) )
11 oveq1 
 |-  ( x = e -> ( x ( .r ` T ) y ) = ( e ( .r ` T ) y ) )
12 10 11 eqeq12d 
 |-  ( x = e -> ( ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) <-> ( e ( .r ` S ) y ) = ( e ( .r ` T ) y ) ) )
13 oveq2 
 |-  ( y = p -> ( e ( .r ` S ) y ) = ( e ( .r ` S ) p ) )
14 oveq2 
 |-  ( y = p -> ( e ( .r ` T ) y ) = ( e ( .r ` T ) p ) )
15 13 14 eqeq12d 
 |-  ( y = p -> ( ( e ( .r ` S ) y ) = ( e ( .r ` T ) y ) <-> ( e ( .r ` S ) p ) = ( e ( .r ` T ) p ) ) )
16 simplr 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> e e. B )
17 eqidd 
 |-  ( ( ( ( ph /\ e e. B ) /\ p e. B ) /\ x = e ) -> B = B )
18 simpr 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> p e. B )
19 12 15 16 17 18 rspc2vd 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( A. x e. B A. y e. B ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) -> ( e ( .r ` S ) p ) = ( e ( .r ` T ) p ) ) )
20 9 19 mpd 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( e ( .r ` S ) p ) = ( e ( .r ` T ) p ) )
21 20 eqeq1d 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( ( e ( .r ` S ) p ) = p <-> ( e ( .r ` T ) p ) = p ) )
22 oveq1 
 |-  ( x = p -> ( x ( .r ` S ) y ) = ( p ( .r ` S ) y ) )
23 oveq1 
 |-  ( x = p -> ( x ( .r ` T ) y ) = ( p ( .r ` T ) y ) )
24 22 23 eqeq12d 
 |-  ( x = p -> ( ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) <-> ( p ( .r ` S ) y ) = ( p ( .r ` T ) y ) ) )
25 oveq2 
 |-  ( y = e -> ( p ( .r ` S ) y ) = ( p ( .r ` S ) e ) )
26 oveq2 
 |-  ( y = e -> ( p ( .r ` T ) y ) = ( p ( .r ` T ) e ) )
27 25 26 eqeq12d 
 |-  ( y = e -> ( ( p ( .r ` S ) y ) = ( p ( .r ` T ) y ) <-> ( p ( .r ` S ) e ) = ( p ( .r ` T ) e ) ) )
28 eqidd 
 |-  ( ( ( ( ph /\ e e. B ) /\ p e. B ) /\ x = p ) -> B = B )
29 24 27 18 28 16 rspc2vd 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( A. x e. B A. y e. B ( x ( .r ` S ) y ) = ( x ( .r ` T ) y ) -> ( p ( .r ` S ) e ) = ( p ( .r ` T ) e ) ) )
30 9 29 mpd 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( p ( .r ` S ) e ) = ( p ( .r ` T ) e ) )
31 30 eqeq1d 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( ( p ( .r ` S ) e ) = p <-> ( p ( .r ` T ) e ) = p ) )
32 21 31 anbi12d 
 |-  ( ( ( ph /\ e e. B ) /\ p e. B ) -> ( ( ( e ( .r ` S ) p ) = p /\ ( p ( .r ` S ) e ) = p ) <-> ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) )
33 6 32 raleqbidva 
 |-  ( ( ph /\ e e. B ) -> ( A. p e. B ( ( e ( .r ` S ) p ) = p /\ ( p ( .r ` S ) e ) = p ) <-> A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) )
34 33 pm5.32da 
 |-  ( ph -> ( ( e e. B /\ A. p e. B ( ( e ( .r ` S ) p ) = p /\ ( p ( .r ` S ) e ) = p ) ) <-> ( e e. B /\ A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) ) )
35 4 eleq2d 
 |-  ( ph -> ( e e. B <-> e e. ( Base ` T ) ) )
36 35 anbi1d 
 |-  ( ph -> ( ( e e. B /\ A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) <-> ( e e. ( Base ` T ) /\ A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) ) )
37 34 36 bitrd 
 |-  ( ph -> ( ( e e. B /\ A. p e. B ( ( e ( .r ` S ) p ) = p /\ ( p ( .r ` S ) e ) = p ) ) <-> ( e e. ( Base ` T ) /\ A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) ) )
38 37 iotabidv 
 |-  ( ph -> ( iota e ( e e. B /\ A. p e. B ( ( e ( .r ` S ) p ) = p /\ ( p ( .r ` S ) e ) = p ) ) ) = ( iota e ( e e. ( Base ` T ) /\ A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) ) )
39 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
40 39 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
41 eqid 
 |-  ( .r ` S ) = ( .r ` S )
42 39 41 mgpplusg 
 |-  ( .r ` S ) = ( +g ` ( mulGrp ` S ) )
43 eqid 
 |-  ( 0g ` ( mulGrp ` S ) ) = ( 0g ` ( mulGrp ` S ) )
44 40 42 43 grpidval 
 |-  ( 0g ` ( mulGrp ` S ) ) = ( iota e ( e e. B /\ A. p e. B ( ( e ( .r ` S ) p ) = p /\ ( p ( .r ` S ) e ) = p ) ) )
45 eqid 
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
46 eqid 
 |-  ( Base ` T ) = ( Base ` T )
47 45 46 mgpbas 
 |-  ( Base ` T ) = ( Base ` ( mulGrp ` T ) )
48 eqid 
 |-  ( .r ` T ) = ( .r ` T )
49 45 48 mgpplusg 
 |-  ( .r ` T ) = ( +g ` ( mulGrp ` T ) )
50 eqid 
 |-  ( 0g ` ( mulGrp ` T ) ) = ( 0g ` ( mulGrp ` T ) )
51 47 49 50 grpidval 
 |-  ( 0g ` ( mulGrp ` T ) ) = ( iota e ( e e. ( Base ` T ) /\ A. p e. ( Base ` T ) ( ( e ( .r ` T ) p ) = p /\ ( p ( .r ` T ) e ) = p ) ) )
52 38 44 51 3eqtr4g 
 |-  ( ph -> ( 0g ` ( mulGrp ` S ) ) = ( 0g ` ( mulGrp ` T ) ) )
53 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
54 39 53 ringidval 
 |-  ( 1r ` S ) = ( 0g ` ( mulGrp ` S ) )
55 eqid 
 |-  ( 1r ` T ) = ( 1r ` T )
56 45 55 ringidval 
 |-  ( 1r ` T ) = ( 0g ` ( mulGrp ` T ) )
57 52 54 56 3eqtr4g 
 |-  ( ph -> ( 1r ` S ) = ( 1r ` T ) )