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=LIdealR
lidldomn1.t ·˙=R
lidldomn1.1 1˙=1R
lidldomn1.0 0˙=0R
Assertion lidldomn1 RDomnULU0˙IUxUI·˙x=xx·˙I=xI=1˙

Proof

Step Hyp Ref Expression
1 lidldomn1.l L=LIdealR
2 lidldomn1.t ·˙=R
3 lidldomn1.1 1˙=1R
4 lidldomn1.0 0˙=0R
5 domnring RDomnRRing
6 5 3ad2ant1 RDomnULU0˙IURRing
7 simp2l RDomnULU0˙IUUL
8 simp2r RDomnULU0˙IUU0˙
9 1 4 lidlnz RRingULU0˙yUy0˙
10 6 7 8 9 syl3anc RDomnULU0˙IUyUy0˙
11 oveq2 x=yI·˙x=I·˙y
12 id x=yx=y
13 11 12 eqeq12d x=yI·˙x=xI·˙y=y
14 oveq1 x=yx·˙I=y·˙I
15 14 12 eqeq12d x=yx·˙I=xy·˙I=y
16 13 15 anbi12d x=yI·˙x=xx·˙I=xI·˙y=yy·˙I=y
17 16 rspcva yUxUI·˙x=xx·˙I=xI·˙y=yy·˙I=y
18 6 adantr RDomnULU0˙IUyUy0˙RRing
19 eqid BaseR=BaseR
20 19 1 lidlss ULUBaseR
21 20 adantr ULU0˙UBaseR
22 21 3ad2ant2 RDomnULU0˙IUUBaseR
23 22 sseld RDomnULU0˙IUyUyBaseR
24 23 com12 yURDomnULU0˙IUyBaseR
25 24 adantr yUy0˙RDomnULU0˙IUyBaseR
26 25 impcom RDomnULU0˙IUyUy0˙yBaseR
27 19 2 3 ringlidm RRingyBaseR1˙·˙y=y
28 18 26 27 syl2anc RDomnULU0˙IUyUy0˙1˙·˙y=y
29 eqeq2 y=1˙·˙yI·˙y=yI·˙y=1˙·˙y
30 29 eqcoms 1˙·˙y=yI·˙y=yI·˙y=1˙·˙y
31 30 adantl RDomnULU0˙IUyUy0˙1˙·˙y=yI·˙y=yI·˙y=1˙·˙y
32 ringgrp RRingRGrp
33 5 32 syl RDomnRGrp
34 33 3ad2ant1 RDomnULU0˙IURGrp
35 34 adantr RDomnULU0˙IUyUy0˙RGrp
36 21 sseld ULU0˙IUIBaseR
37 36 a1i RDomnULU0˙IUIBaseR
38 37 3imp RDomnULU0˙IUIBaseR
39 38 adantr RDomnULU0˙IUyUy0˙IBaseR
40 19 2 ringcl RRingIBaseRyBaseRI·˙yBaseR
41 18 39 26 40 syl3anc RDomnULU0˙IUyUy0˙I·˙yBaseR
42 19 3 ringidcl RRing1˙BaseR
43 5 42 syl RDomn1˙BaseR
44 43 3ad2ant1 RDomnULU0˙IU1˙BaseR
45 44 adantr RDomnULU0˙IUyUy0˙1˙BaseR
46 19 2 ringcl RRing1˙BaseRyBaseR1˙·˙yBaseR
47 18 45 26 46 syl3anc RDomnULU0˙IUyUy0˙1˙·˙yBaseR
48 eqid -R=-R
49 19 4 48 grpsubeq0 RGrpI·˙yBaseR1˙·˙yBaseRI·˙y-R1˙·˙y=0˙I·˙y=1˙·˙y
50 35 41 47 49 syl3anc RDomnULU0˙IUyUy0˙I·˙y-R1˙·˙y=0˙I·˙y=1˙·˙y
51 19 2 48 18 39 45 26 rngsubdir RDomnULU0˙IUyUy0˙I-R1˙·˙y=I·˙y-R1˙·˙y
52 51 eqeq1d RDomnULU0˙IUyUy0˙I-R1˙·˙y=0˙I·˙y-R1˙·˙y=0˙
53 simpl1 RDomnULU0˙IUyUy0˙RDomn
54 34 38 44 3jca RDomnULU0˙IURGrpIBaseR1˙BaseR
55 54 adantr RDomnULU0˙IUyUy0˙RGrpIBaseR1˙BaseR
56 19 48 grpsubcl RGrpIBaseR1˙BaseRI-R1˙BaseR
57 55 56 syl RDomnULU0˙IUyUy0˙I-R1˙BaseR
58 19 2 4 domneq0 RDomnI-R1˙BaseRyBaseRI-R1˙·˙y=0˙I-R1˙=0˙y=0˙
59 53 57 26 58 syl3anc RDomnULU0˙IUyUy0˙I-R1˙·˙y=0˙I-R1˙=0˙y=0˙
60 19 4 48 grpsubeq0 RGrpIBaseR1˙BaseRI-R1˙=0˙I=1˙
61 55 60 syl RDomnULU0˙IUyUy0˙I-R1˙=0˙I=1˙
62 61 biimpd RDomnULU0˙IUyUy0˙I-R1˙=0˙I=1˙
63 eqneqall y=0˙y0˙I=1˙
64 63 com12 y0˙y=0˙I=1˙
65 64 adantl yUy0˙y=0˙I=1˙
66 65 adantl RDomnULU0˙IUyUy0˙y=0˙I=1˙
67 62 66 jaod RDomnULU0˙IUyUy0˙I-R1˙=0˙y=0˙I=1˙
68 59 67 sylbid RDomnULU0˙IUyUy0˙I-R1˙·˙y=0˙I=1˙
69 52 68 sylbird RDomnULU0˙IUyUy0˙I·˙y-R1˙·˙y=0˙I=1˙
70 50 69 sylbird RDomnULU0˙IUyUy0˙I·˙y=1˙·˙yI=1˙
71 70 adantr RDomnULU0˙IUyUy0˙1˙·˙y=yI·˙y=1˙·˙yI=1˙
72 31 71 sylbid RDomnULU0˙IUyUy0˙1˙·˙y=yI·˙y=yI=1˙
73 28 72 mpdan RDomnULU0˙IUyUy0˙I·˙y=yI=1˙
74 73 ex RDomnULU0˙IUyUy0˙I·˙y=yI=1˙
75 74 com13 I·˙y=yyUy0˙RDomnULU0˙IUI=1˙
76 75 expd I·˙y=yyUy0˙RDomnULU0˙IUI=1˙
77 76 adantr I·˙y=yy·˙I=yyUy0˙RDomnULU0˙IUI=1˙
78 17 77 syl yUxUI·˙x=xx·˙I=xyUy0˙RDomnULU0˙IUI=1˙
79 78 ex yUxUI·˙x=xx·˙I=xyUy0˙RDomnULU0˙IUI=1˙
80 79 pm2.43b xUI·˙x=xx·˙I=xyUy0˙RDomnULU0˙IUI=1˙
81 80 com14 RDomnULU0˙IUyUy0˙xUI·˙x=xx·˙I=xI=1˙
82 81 imp RDomnULU0˙IUyUy0˙xUI·˙x=xx·˙I=xI=1˙
83 82 rexlimdva RDomnULU0˙IUyUy0˙xUI·˙x=xx·˙I=xI=1˙
84 10 83 mpd RDomnULU0˙IUxUI·˙x=xx·˙I=xI=1˙