Metamath Proof Explorer

Theorem lidldomn1

Description: If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020)

Ref Expression
Hypotheses lidldomn1.l 
|- L = ( LIdeal ` R )
lidldomn1.t 
|- .x. = ( .r ` R )
lidldomn1.1 
|- .1. = ( 1r ` R )
lidldomn1.0 
|- .0. = ( 0g ` R )
Assertion lidldomn1 
|- ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> I = .1. ) )

Proof

Step Hyp Ref Expression
1 lidldomn1.l 
 |-  L = ( LIdeal ` R )
2 lidldomn1.t 
 |-  .x. = ( .r ` R )
3 lidldomn1.1 
 |-  .1. = ( 1r ` R )
4 lidldomn1.0 
 |-  .0. = ( 0g ` R )
5 domnring 
 |-  ( R e. Domn -> R e. Ring )
6 5 3ad2ant1 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> R e. Ring )
7 simp2l 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> U e. L )
8 simp2r 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> U =/= { .0. } )
9 1 4 lidlnz 
 |-  ( ( R e. Ring /\ U e. L /\ U =/= { .0. } ) -> E. y e. U y =/= .0. )
10 6 7 8 9 syl3anc 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> E. y e. U y =/= .0. )
11 oveq2 
 |-  ( x = y -> ( I .x. x ) = ( I .x. y ) )
12 id 
 |-  ( x = y -> x = y )
13 11 12 eqeq12d 
 |-  ( x = y -> ( ( I .x. x ) = x <-> ( I .x. y ) = y ) )
14 oveq1 
 |-  ( x = y -> ( x .x. I ) = ( y .x. I ) )
15 14 12 eqeq12d 
 |-  ( x = y -> ( ( x .x. I ) = x <-> ( y .x. I ) = y ) )
16 13 15 anbi12d 
 |-  ( x = y -> ( ( ( I .x. x ) = x /\ ( x .x. I ) = x ) <-> ( ( I .x. y ) = y /\ ( y .x. I ) = y ) ) )
17 16 rspcva 
 |-  ( ( y e. U /\ A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) -> ( ( I .x. y ) = y /\ ( y .x. I ) = y ) )
18 6 adantr 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> R e. Ring )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 19 1 lidlss 
 |-  ( U e. L -> U C_ ( Base ` R ) )
21 20 adantr 
 |-  ( ( U e. L /\ U =/= { .0. } ) -> U C_ ( Base ` R ) )
22 21 3ad2ant2 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> U C_ ( Base ` R ) )
23 22 sseld 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( y e. U -> y e. ( Base ` R ) ) )
24 23 com12 
 |-  ( y e. U -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> y e. ( Base ` R ) ) )
25 24 adantr 
 |-  ( ( y e. U /\ y =/= .0. ) -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> y e. ( Base ` R ) ) )
26 25 impcom 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> y e. ( Base ` R ) )
27 19 2 3 ringlidm 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) ) -> ( .1. .x. y ) = y )
28 18 26 27 syl2anc 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( .1. .x. y ) = y )
29 eqeq2 
 |-  ( y = ( .1. .x. y ) -> ( ( I .x. y ) = y <-> ( I .x. y ) = ( .1. .x. y ) ) )
30 29 eqcoms 
 |-  ( ( .1. .x. y ) = y -> ( ( I .x. y ) = y <-> ( I .x. y ) = ( .1. .x. y ) ) )
31 30 adantl 
 |-  ( ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) /\ ( .1. .x. y ) = y ) -> ( ( I .x. y ) = y <-> ( I .x. y ) = ( .1. .x. y ) ) )
32 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
33 5 32 syl 
 |-  ( R e. Domn -> R e. Grp )
34 33 3ad2ant1 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> R e. Grp )
35 34 adantr 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> R e. Grp )
36 21 sseld 
 |-  ( ( U e. L /\ U =/= { .0. } ) -> ( I e. U -> I e. ( Base ` R ) ) )
37 36 a1i 
 |-  ( R e. Domn -> ( ( U e. L /\ U =/= { .0. } ) -> ( I e. U -> I e. ( Base ` R ) ) ) )
38 37 3imp 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I e. ( Base ` R ) )
39 38 adantr 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> I e. ( Base ` R ) )
40 19 2 ringcl 
 |-  ( ( R e. Ring /\ I e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( I .x. y ) e. ( Base ` R ) )
41 18 39 26 40 syl3anc 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( I .x. y ) e. ( Base ` R ) )
42 19 3 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
43 5 42 syl 
 |-  ( R e. Domn -> .1. e. ( Base ` R ) )
44 43 3ad2ant1 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> .1. e. ( Base ` R ) )
45 44 adantr 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> .1. e. ( Base ` R ) )
46 19 2 ringcl 
 |-  ( ( R e. Ring /\ .1. e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( .1. .x. y ) e. ( Base ` R ) )
47 18 45 26 46 syl3anc 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( .1. .x. y ) e. ( Base ` R ) )
48 eqid 
 |-  ( -g ` R ) = ( -g ` R )
49 19 4 48 grpsubeq0 
 |-  ( ( R e. Grp /\ ( I .x. y ) e. ( Base ` R ) /\ ( .1. .x. y ) e. ( Base ` R ) ) -> ( ( ( I .x. y ) ( -g ` R ) ( .1. .x. y ) ) = .0. <-> ( I .x. y ) = ( .1. .x. y ) ) )
50 35 41 47 49 syl3anc 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( ( I .x. y ) ( -g ` R ) ( .1. .x. y ) ) = .0. <-> ( I .x. y ) = ( .1. .x. y ) ) )
51 19 2 48 18 39 45 26 rngsubdir 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( I ( -g ` R ) .1. ) .x. y ) = ( ( I .x. y ) ( -g ` R ) ( .1. .x. y ) ) )
52 51 eqeq1d 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( ( I ( -g ` R ) .1. ) .x. y ) = .0. <-> ( ( I .x. y ) ( -g ` R ) ( .1. .x. y ) ) = .0. ) )
53 simpl1 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> R e. Domn )
54 34 38 44 3jca 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( R e. Grp /\ I e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) )
55 54 adantr 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( R e. Grp /\ I e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) )
56 19 48 grpsubcl 
 |-  ( ( R e. Grp /\ I e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) -> ( I ( -g ` R ) .1. ) e. ( Base ` R ) )
57 55 56 syl 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( I ( -g ` R ) .1. ) e. ( Base ` R ) )
58 19 2 4 domneq0 
 |-  ( ( R e. Domn /\ ( I ( -g ` R ) .1. ) e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( ( I ( -g ` R ) .1. ) .x. y ) = .0. <-> ( ( I ( -g ` R ) .1. ) = .0. \/ y = .0. ) ) )
59 53 57 26 58 syl3anc 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( ( I ( -g ` R ) .1. ) .x. y ) = .0. <-> ( ( I ( -g ` R ) .1. ) = .0. \/ y = .0. ) ) )
60 19 4 48 grpsubeq0 
 |-  ( ( R e. Grp /\ I e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) -> ( ( I ( -g ` R ) .1. ) = .0. <-> I = .1. ) )
61 55 60 syl 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( I ( -g ` R ) .1. ) = .0. <-> I = .1. ) )
62 61 biimpd 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( I ( -g ` R ) .1. ) = .0. -> I = .1. ) )
63 eqneqall 
 |-  ( y = .0. -> ( y =/= .0. -> I = .1. ) )
64 63 com12 
 |-  ( y =/= .0. -> ( y = .0. -> I = .1. ) )
65 64 adantl 
 |-  ( ( y e. U /\ y =/= .0. ) -> ( y = .0. -> I = .1. ) )
66 65 adantl 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( y = .0. -> I = .1. ) )
67 62 66 jaod 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( ( I ( -g ` R ) .1. ) = .0. \/ y = .0. ) -> I = .1. ) )
68 59 67 sylbid 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( ( I ( -g ` R ) .1. ) .x. y ) = .0. -> I = .1. ) )
69 52 68 sylbird 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( ( I .x. y ) ( -g ` R ) ( .1. .x. y ) ) = .0. -> I = .1. ) )
70 50 69 sylbird 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( I .x. y ) = ( .1. .x. y ) -> I = .1. ) )
71 70 adantr 
 |-  ( ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) /\ ( .1. .x. y ) = y ) -> ( ( I .x. y ) = ( .1. .x. y ) -> I = .1. ) )
72 31 71 sylbid 
 |-  ( ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) /\ ( .1. .x. y ) = y ) -> ( ( I .x. y ) = y -> I = .1. ) )
73 28 72 mpdan 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ ( y e. U /\ y =/= .0. ) ) -> ( ( I .x. y ) = y -> I = .1. ) )
74 73 ex 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( ( y e. U /\ y =/= .0. ) -> ( ( I .x. y ) = y -> I = .1. ) ) )
75 74 com13 
 |-  ( ( I .x. y ) = y -> ( ( y e. U /\ y =/= .0. ) -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I = .1. ) ) )
76 75 expd 
 |-  ( ( I .x. y ) = y -> ( y e. U -> ( y =/= .0. -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I = .1. ) ) ) )
77 76 adantr 
 |-  ( ( ( I .x. y ) = y /\ ( y .x. I ) = y ) -> ( y e. U -> ( y =/= .0. -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I = .1. ) ) ) )
78 17 77 syl 
 |-  ( ( y e. U /\ A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) -> ( y e. U -> ( y =/= .0. -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I = .1. ) ) ) )
79 78 ex 
 |-  ( y e. U -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> ( y e. U -> ( y =/= .0. -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I = .1. ) ) ) ) )
80 79 pm2.43b 
 |-  ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> ( y e. U -> ( y =/= .0. -> ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> I = .1. ) ) ) )
81 80 com14 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( y e. U -> ( y =/= .0. -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> I = .1. ) ) ) )
82 81 imp 
 |-  ( ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) /\ y e. U ) -> ( y =/= .0. -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> I = .1. ) ) )
83 82 rexlimdva 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( E. y e. U y =/= .0. -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> I = .1. ) ) )
84 10 83 mpd 
 |-  ( ( R e. Domn /\ ( U e. L /\ U =/= { .0. } ) /\ I e. U ) -> ( A. x e. U ( ( I .x. x ) = x /\ ( x .x. I ) = x ) -> I = .1. ) )