Metamath Proof Explorer

Theorem rngurd

Description: Deduce the unit of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016)

Ref Expression
Hypotheses rngurd.b 
|- ( ph -> B = ( Base ` R ) )
rngurd.p 
|- ( ph -> .x. = ( .r ` R ) )
rngurd.z 
|- ( ph -> .1. e. B )
rngurd.i 
|- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )
rngurd.j 
|- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )
Assertion rngurd 
|- ( ph -> .1. = ( 1r ` R ) )

Proof

Step Hyp Ref Expression
1 rngurd.b 
 |-  ( ph -> B = ( Base ` R ) )
2 rngurd.p 
 |-  ( ph -> .x. = ( .r ` R ) )
3 rngurd.z 
 |-  ( ph -> .1. e. B )
4 rngurd.i 
 |-  ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )
5 rngurd.j 
 |-  ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 6 7 8 dfur2 
 |-  ( 1r ` R ) = ( iota e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) )
10 3 1 eleqtrd 
 |-  ( ph -> .1. e. ( Base ` R ) )
11 4 5 jca 
 |-  ( ( ph /\ x e. B ) -> ( ( .1. .x. x ) = x /\ ( x .x. .1. ) = x ) )
12 11 ralrimiva 
 |-  ( ph -> A. x e. B ( ( .1. .x. x ) = x /\ ( x .x. .1. ) = x ) )
13 2 adantr 
 |-  ( ( ph /\ x e. B ) -> .x. = ( .r ` R ) )
14 13 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( .1. .x. x ) = ( .1. ( .r ` R ) x ) )
15 14 eqeq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( .1. .x. x ) = x <-> ( .1. ( .r ` R ) x ) = x ) )
16 13 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( x .x. .1. ) = ( x ( .r ` R ) .1. ) )
17 16 eqeq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( x .x. .1. ) = x <-> ( x ( .r ` R ) .1. ) = x ) )
18 15 17 anbi12d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( .1. .x. x ) = x /\ ( x .x. .1. ) = x ) <-> ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) )
19 1 18 raleqbidva 
 |-  ( ph -> ( A. x e. B ( ( .1. .x. x ) = x /\ ( x .x. .1. ) = x ) <-> A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) )
20 12 19 mpbid 
 |-  ( ph -> A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) )
21 1 eleq2d 
 |-  ( ph -> ( e e. B <-> e e. ( Base ` R ) ) )
22 13 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( e .x. x ) = ( e ( .r ` R ) x ) )
23 22 eqeq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( e .x. x ) = x <-> ( e ( .r ` R ) x ) = x ) )
24 13 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( x .x. e ) = ( x ( .r ` R ) e ) )
25 24 eqeq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( x .x. e ) = x <-> ( x ( .r ` R ) e ) = x ) )
26 23 25 anbi12d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( e .x. x ) = x /\ ( x .x. e ) = x ) <-> ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) )
27 1 26 raleqbidva 
 |-  ( ph -> ( A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) <-> A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) )
28 21 27 anbi12d 
 |-  ( ph -> ( ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) <-> ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) ) )
29 4 ralrimiva 
 |-  ( ph -> A. x e. B ( .1. .x. x ) = x )
30 29 adantr 
 |-  ( ( ph /\ e e. B ) -> A. x e. B ( .1. .x. x ) = x )
31 simpr 
 |-  ( ( ph /\ e e. B ) -> e e. B )
32 simpr 
 |-  ( ( ( ph /\ e e. B ) /\ x = e ) -> x = e )
33 32 oveq2d 
 |-  ( ( ( ph /\ e e. B ) /\ x = e ) -> ( .1. .x. x ) = ( .1. .x. e ) )
34 33 32 eqeq12d 
 |-  ( ( ( ph /\ e e. B ) /\ x = e ) -> ( ( .1. .x. x ) = x <-> ( .1. .x. e ) = e ) )
35 31 34 rspcdv 
 |-  ( ( ph /\ e e. B ) -> ( A. x e. B ( .1. .x. x ) = x -> ( .1. .x. e ) = e ) )
36 30 35 mpd 
 |-  ( ( ph /\ e e. B ) -> ( .1. .x. e ) = e )
37 36 adantrr 
 |-  ( ( ph /\ ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) -> ( .1. .x. e ) = e )
38 3 adantr 
 |-  ( ( ph /\ ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) -> .1. e. B )
39 simprr 
 |-  ( ( ph /\ ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) -> A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) )
40 oveq2 
 |-  ( x = .1. -> ( e .x. x ) = ( e .x. .1. ) )
41 id 
 |-  ( x = .1. -> x = .1. )
42 40 41 eqeq12d 
 |-  ( x = .1. -> ( ( e .x. x ) = x <-> ( e .x. .1. ) = .1. ) )
43 oveq1 
 |-  ( x = .1. -> ( x .x. e ) = ( .1. .x. e ) )
44 43 41 eqeq12d 
 |-  ( x = .1. -> ( ( x .x. e ) = x <-> ( .1. .x. e ) = .1. ) )
45 42 44 anbi12d 
 |-  ( x = .1. -> ( ( ( e .x. x ) = x /\ ( x .x. e ) = x ) <-> ( ( e .x. .1. ) = .1. /\ ( .1. .x. e ) = .1. ) ) )
46 45 rspcva 
 |-  ( ( .1. e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) -> ( ( e .x. .1. ) = .1. /\ ( .1. .x. e ) = .1. ) )
47 46 simprd 
 |-  ( ( .1. e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) -> ( .1. .x. e ) = .1. )
48 38 39 47 syl2anc 
 |-  ( ( ph /\ ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) -> ( .1. .x. e ) = .1. )
49 37 48 eqtr3d 
 |-  ( ( ph /\ ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) -> e = .1. )
50 49 ex 
 |-  ( ph -> ( ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) -> e = .1. ) )
51 28 50 sylbird 
 |-  ( ph -> ( ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) -> e = .1. ) )
52 51 alrimiv 
 |-  ( ph -> A. e ( ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) -> e = .1. ) )
53 eleq1 
 |-  ( e = .1. -> ( e e. ( Base ` R ) <-> .1. e. ( Base ` R ) ) )
54 oveq1 
 |-  ( e = .1. -> ( e ( .r ` R ) x ) = ( .1. ( .r ` R ) x ) )
55 54 eqeq1d 
 |-  ( e = .1. -> ( ( e ( .r ` R ) x ) = x <-> ( .1. ( .r ` R ) x ) = x ) )
56 55 ovanraleqv 
 |-  ( e = .1. -> ( A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) <-> A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) )
57 53 56 anbi12d 
 |-  ( e = .1. -> ( ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) <-> ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) ) )
58 57 eqeu 
 |-  ( ( .1. e. ( Base ` R ) /\ ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) /\ A. e ( ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) -> e = .1. ) ) -> E! e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) )
59 10 10 20 52 58 syl121anc 
 |-  ( ph -> E! e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) )
60 57 iota2 
 |-  ( ( .1. e. B /\ E! e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) ) -> ( ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) <-> ( iota e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) ) = .1. ) )
61 3 59 60 syl2anc 
 |-  ( ph -> ( ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( .1. ( .r ` R ) x ) = x /\ ( x ( .r ` R ) .1. ) = x ) ) <-> ( iota e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) ) = .1. ) )
62 10 20 61 mpbi2and 
 |-  ( ph -> ( iota e ( e e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( e ( .r ` R ) x ) = x /\ ( x ( .r ` R ) e ) = x ) ) ) = .1. )
63 9 62 eqtr2id 
 |-  ( ph -> .1. = ( 1r ` R ) )