Metamath Proof Explorer

Theorem prnc

Description: A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses prnc.1 ⊢G=1st⁡R
prnc.2 ⊢H=2nd⁡R
prnc.3 ⊢X=ran⁡G
Assertion prnc ⊢R∈CRingOps∧A∈X→RIdlGenA=x∈X|∃y∈Xx=yHA

Proof

Step Hyp Ref Expression
1 prnc.1 ⊢G=1st⁡R
2 prnc.2 ⊢H=2nd⁡R
3 prnc.3 ⊢X=ran⁡G
4 crngorngo ⊢R∈CRingOps→R∈RingOps
5 ssrab2 ⊢x∈X|∃y∈Xx=yHA⊆X
6 5 a1i ⊢R∈RingOps∧A∈X→x∈X|∃y∈Xx=yHA⊆X
7 eqid ⊢GId⁡G=GId⁡G
8 1 3 7 rngo0cl ⊢R∈RingOps→GId⁡G∈X
9 8 adantr ⊢R∈RingOps∧A∈X→GId⁡G∈X
10 7 3 1 2 rngolz ⊢R∈RingOps∧A∈X→GId⁡GHA=GId⁡G
11 10 eqcomd ⊢R∈RingOps∧A∈X→GId⁡G=GId⁡GHA
12 oveq1 ⊢y=GId⁡G→yHA=GId⁡GHA
13 12 rspceeqv ⊢GId⁡G∈X∧GId⁡G=GId⁡GHA→∃y∈XGId⁡G=yHA
14 9 11 13 syl2anc ⊢R∈RingOps∧A∈X→∃y∈XGId⁡G=yHA
15 eqeq1 ⊢x=GId⁡G→x=yHA↔GId⁡G=yHA
16 15 rexbidv ⊢x=GId⁡G→∃y∈Xx=yHA↔∃y∈XGId⁡G=yHA
17 16 elrab ⊢GId⁡G∈x∈X|∃y∈Xx=yHA↔GId⁡G∈X∧∃y∈XGId⁡G=yHA
18 9 14 17 sylanbrc ⊢R∈RingOps∧A∈X→GId⁡G∈x∈X|∃y∈Xx=yHA
19 eqeq1 ⊢x=u→x=yHA↔u=yHA
20 19 rexbidv ⊢x=u→∃y∈Xx=yHA↔∃y∈Xu=yHA
21 oveq1 ⊢y=r→yHA=rHA
22 21 eqeq2d ⊢y=r→u=yHA↔u=rHA
23 22 cbvrexvw ⊢∃y∈Xu=yHA↔∃r∈Xu=rHA
24 20 23 bitrdi ⊢x=u→∃y∈Xx=yHA↔∃r∈Xu=rHA
25 24 elrab ⊢u∈x∈X|∃y∈Xx=yHA↔u∈X∧∃r∈Xu=rHA
26 eqeq1 ⊢x=v→x=yHA↔v=yHA
27 26 rexbidv ⊢x=v→∃y∈Xx=yHA↔∃y∈Xv=yHA
28 oveq1 ⊢y=s→yHA=sHA
29 28 eqeq2d ⊢y=s→v=yHA↔v=sHA
30 29 cbvrexvw ⊢∃y∈Xv=yHA↔∃s∈Xv=sHA
31 27 30 bitrdi ⊢x=v→∃y∈Xx=yHA↔∃s∈Xv=sHA
32 31 elrab ⊢v∈x∈X|∃y∈Xx=yHA↔v∈X∧∃s∈Xv=sHA
33 1 2 3 rngodir ⊢R∈RingOps∧r∈X∧s∈X∧A∈X→rGsHA=rHAGsHA
34 33 3exp2 ⊢R∈RingOps→r∈X→s∈X→A∈X→rGsHA=rHAGsHA
35 34 imp42 ⊢R∈RingOps∧r∈X∧s∈X∧A∈X→rGsHA=rHAGsHA
36 1 3 rngogcl ⊢R∈RingOps∧r∈X∧s∈X→rGs∈X
37 36 3expib ⊢R∈RingOps→r∈X∧s∈X→rGs∈X
38 37 imdistani ⊢R∈RingOps∧r∈X∧s∈X→R∈RingOps∧rGs∈X
39 1 2 3 rngocl ⊢R∈RingOps∧rGs∈X∧A∈X→rGsHA∈X
40 39 3expa ⊢R∈RingOps∧rGs∈X∧A∈X→rGsHA∈X
41 eqid ⊢rGsHA=rGsHA
42 oveq1 ⊢y=rGs→yHA=rGsHA
43 42 rspceeqv ⊢rGs∈X∧rGsHA=rGsHA→∃y∈XrGsHA=yHA
44 41 43 mpan2 ⊢rGs∈X→∃y∈XrGsHA=yHA
45 44 ad2antlr ⊢R∈RingOps∧rGs∈X∧A∈X→∃y∈XrGsHA=yHA
46 eqeq1 ⊢x=rGsHA→x=yHA↔rGsHA=yHA
47 46 rexbidv ⊢x=rGsHA→∃y∈Xx=yHA↔∃y∈XrGsHA=yHA
48 47 elrab ⊢rGsHA∈x∈X|∃y∈Xx=yHA↔rGsHA∈X∧∃y∈XrGsHA=yHA
49 40 45 48 sylanbrc ⊢R∈RingOps∧rGs∈X∧A∈X→rGsHA∈x∈X|∃y∈Xx=yHA
50 38 49 sylan ⊢R∈RingOps∧r∈X∧s∈X∧A∈X→rGsHA∈x∈X|∃y∈Xx=yHA
51 35 50 eqeltrrd ⊢R∈RingOps∧r∈X∧s∈X∧A∈X→rHAGsHA∈x∈X|∃y∈Xx=yHA
52 51 an32s ⊢R∈RingOps∧A∈X∧r∈X∧s∈X→rHAGsHA∈x∈X|∃y∈Xx=yHA
53 52 anassrs ⊢R∈RingOps∧A∈X∧r∈X∧s∈X→rHAGsHA∈x∈X|∃y∈Xx=yHA
54 oveq2 ⊢v=sHA→rHAGv=rHAGsHA
55 54 eleq1d ⊢v=sHA→rHAGv∈x∈X|∃y∈Xx=yHA↔rHAGsHA∈x∈X|∃y∈Xx=yHA
56 53 55 syl5ibrcom ⊢R∈RingOps∧A∈X∧r∈X∧s∈X→v=sHA→rHAGv∈x∈X|∃y∈Xx=yHA
57 56 rexlimdva ⊢R∈RingOps∧A∈X∧r∈X→∃s∈Xv=sHA→rHAGv∈x∈X|∃y∈Xx=yHA
58 57 adantld ⊢R∈RingOps∧A∈X∧r∈X→v∈X∧∃s∈Xv=sHA→rHAGv∈x∈X|∃y∈Xx=yHA
59 32 58 biimtrid ⊢R∈RingOps∧A∈X∧r∈X→v∈x∈X|∃y∈Xx=yHA→rHAGv∈x∈X|∃y∈Xx=yHA
60 59 ralrimiv ⊢R∈RingOps∧A∈X∧r∈X→∀v∈x∈X|∃y∈Xx=yHArHAGv∈x∈X|∃y∈Xx=yHA
61 1 2 3 rngoass ⊢R∈RingOps∧w∈X∧r∈X∧A∈X→wHrHA=wHrHA
62 61 3exp2 ⊢R∈RingOps→w∈X→r∈X→A∈X→wHrHA=wHrHA
63 62 imp42 ⊢R∈RingOps∧w∈X∧r∈X∧A∈X→wHrHA=wHrHA
64 63 an32s ⊢R∈RingOps∧A∈X∧w∈X∧r∈X→wHrHA=wHrHA
65 1 2 3 rngocl ⊢R∈RingOps∧w∈X∧r∈X→wHr∈X
66 65 3expib ⊢R∈RingOps→w∈X∧r∈X→wHr∈X
67 66 imdistani ⊢R∈RingOps∧w∈X∧r∈X→R∈RingOps∧wHr∈X
68 1 2 3 rngocl ⊢R∈RingOps∧wHr∈X∧A∈X→wHrHA∈X
69 68 3expa ⊢R∈RingOps∧wHr∈X∧A∈X→wHrHA∈X
70 eqid ⊢wHrHA=wHrHA
71 oveq1 ⊢y=wHr→yHA=wHrHA
72 71 rspceeqv ⊢wHr∈X∧wHrHA=wHrHA→∃y∈XwHrHA=yHA
73 70 72 mpan2 ⊢wHr∈X→∃y∈XwHrHA=yHA
74 73 ad2antlr ⊢R∈RingOps∧wHr∈X∧A∈X→∃y∈XwHrHA=yHA
75 eqeq1 ⊢x=wHrHA→x=yHA↔wHrHA=yHA
76 75 rexbidv ⊢x=wHrHA→∃y∈Xx=yHA↔∃y∈XwHrHA=yHA
77 76 elrab ⊢wHrHA∈x∈X|∃y∈Xx=yHA↔wHrHA∈X∧∃y∈XwHrHA=yHA
78 69 74 77 sylanbrc ⊢R∈RingOps∧wHr∈X∧A∈X→wHrHA∈x∈X|∃y∈Xx=yHA
79 67 78 sylan ⊢R∈RingOps∧w∈X∧r∈X∧A∈X→wHrHA∈x∈X|∃y∈Xx=yHA
80 79 an32s ⊢R∈RingOps∧A∈X∧w∈X∧r∈X→wHrHA∈x∈X|∃y∈Xx=yHA
81 64 80 eqeltrrd ⊢R∈RingOps∧A∈X∧w∈X∧r∈X→wHrHA∈x∈X|∃y∈Xx=yHA
82 81 anass1rs ⊢R∈RingOps∧A∈X∧r∈X∧w∈X→wHrHA∈x∈X|∃y∈Xx=yHA
83 82 ralrimiva ⊢R∈RingOps∧A∈X∧r∈X→∀w∈XwHrHA∈x∈X|∃y∈Xx=yHA
84 60 83 jca ⊢R∈RingOps∧A∈X∧r∈X→∀v∈x∈X|∃y∈Xx=yHArHAGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHrHA∈x∈X|∃y∈Xx=yHA
85 oveq1 ⊢u=rHA→uGv=rHAGv
86 85 eleq1d ⊢u=rHA→uGv∈x∈X|∃y∈Xx=yHA↔rHAGv∈x∈X|∃y∈Xx=yHA
87 86 ralbidv ⊢u=rHA→∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA↔∀v∈x∈X|∃y∈Xx=yHArHAGv∈x∈X|∃y∈Xx=yHA
88 oveq2 ⊢u=rHA→wHu=wHrHA
89 88 eleq1d ⊢u=rHA→wHu∈x∈X|∃y∈Xx=yHA↔wHrHA∈x∈X|∃y∈Xx=yHA
90 89 ralbidv ⊢u=rHA→∀w∈XwHu∈x∈X|∃y∈Xx=yHA↔∀w∈XwHrHA∈x∈X|∃y∈Xx=yHA
91 87 90 anbi12d ⊢u=rHA→∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA↔∀v∈x∈X|∃y∈Xx=yHArHAGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHrHA∈x∈X|∃y∈Xx=yHA
92 84 91 syl5ibrcom ⊢R∈RingOps∧A∈X∧r∈X→u=rHA→∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
93 92 rexlimdva ⊢R∈RingOps∧A∈X→∃r∈Xu=rHA→∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
94 93 adantld ⊢R∈RingOps∧A∈X→u∈X∧∃r∈Xu=rHA→∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
95 25 94 biimtrid ⊢R∈RingOps∧A∈X→u∈x∈X|∃y∈Xx=yHA→∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
96 95 ralrimiv ⊢R∈RingOps∧A∈X→∀u∈x∈X|∃y∈Xx=yHA∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
97 6 18 96 3jca ⊢R∈RingOps∧A∈X→x∈X|∃y∈Xx=yHA⊆X∧GId⁡G∈x∈X|∃y∈Xx=yHA∧∀u∈x∈X|∃y∈Xx=yHA∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
98 4 97 sylan ⊢R∈CRingOps∧A∈X→x∈X|∃y∈Xx=yHA⊆X∧GId⁡G∈x∈X|∃y∈Xx=yHA∧∀u∈x∈X|∃y∈Xx=yHA∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
99 1 2 3 7 isidlc ⊢R∈CRingOps→x∈X|∃y∈Xx=yHA∈Idl⁡R↔x∈X|∃y∈Xx=yHA⊆X∧GId⁡G∈x∈X|∃y∈Xx=yHA∧∀u∈x∈X|∃y∈Xx=yHA∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
100 99 adantr ⊢R∈CRingOps∧A∈X→x∈X|∃y∈Xx=yHA∈Idl⁡R↔x∈X|∃y∈Xx=yHA⊆X∧GId⁡G∈x∈X|∃y∈Xx=yHA∧∀u∈x∈X|∃y∈Xx=yHA∀v∈x∈X|∃y∈Xx=yHAuGv∈x∈X|∃y∈Xx=yHA∧∀w∈XwHu∈x∈X|∃y∈Xx=yHA
101 98 100 mpbird ⊢R∈CRingOps∧A∈X→x∈X|∃y∈Xx=yHA∈Idl⁡R
102 simpr ⊢R∈CRingOps∧A∈X→A∈X
103 1 rneqi ⊢ran⁡G=ran⁡1st⁡R
104 3 103 eqtri ⊢X=ran⁡1st⁡R
105 eqid ⊢GId⁡H=GId⁡H
106 104 2 105 rngo1cl ⊢R∈RingOps→GId⁡H∈X
107 106 adantr ⊢R∈RingOps∧A∈X→GId⁡H∈X
108 2 104 105 rngolidm ⊢R∈RingOps∧A∈X→GId⁡HHA=A
109 108 eqcomd ⊢R∈RingOps∧A∈X→A=GId⁡HHA
110 oveq1 ⊢y=GId⁡H→yHA=GId⁡HHA
111 110 rspceeqv ⊢GId⁡H∈X∧A=GId⁡HHA→∃y∈XA=yHA
112 107 109 111 syl2anc ⊢R∈RingOps∧A∈X→∃y∈XA=yHA
113 4 112 sylan ⊢R∈CRingOps∧A∈X→∃y∈XA=yHA
114 eqeq1 ⊢x=A→x=yHA↔A=yHA
115 114 rexbidv ⊢x=A→∃y∈Xx=yHA↔∃y∈XA=yHA
116 115 elrab ⊢A∈x∈X|∃y∈Xx=yHA↔A∈X∧∃y∈XA=yHA
117 102 113 116 sylanbrc ⊢R∈CRingOps∧A∈X→A∈x∈X|∃y∈Xx=yHA
118 117 snssd ⊢R∈CRingOps∧A∈X→A⊆x∈X|∃y∈Xx=yHA
119 snssg ⊢A∈X→A∈j↔A⊆j
120 119 biimpar ⊢A∈X∧A⊆j→A∈j
121 1 2 3 idllmulcl ⊢R∈RingOps∧j∈Idl⁡R∧A∈j∧y∈X→yHA∈j
122 121 anassrs ⊢R∈RingOps∧j∈Idl⁡R∧A∈j∧y∈X→yHA∈j
123 eleq1 ⊢x=yHA→x∈j↔yHA∈j
124 122 123 syl5ibrcom ⊢R∈RingOps∧j∈Idl⁡R∧A∈j∧y∈X→x=yHA→x∈j
125 124 rexlimdva ⊢R∈RingOps∧j∈Idl⁡R∧A∈j→∃y∈Xx=yHA→x∈j
126 125 adantr ⊢R∈RingOps∧j∈Idl⁡R∧A∈j∧x∈X→∃y∈Xx=yHA→x∈j
127 126 ralrimiva ⊢R∈RingOps∧j∈Idl⁡R∧A∈j→∀x∈X∃y∈Xx=yHA→x∈j
128 rabss ⊢x∈X|∃y∈Xx=yHA⊆j↔∀x∈X∃y∈Xx=yHA→x∈j
129 127 128 sylibr ⊢R∈RingOps∧j∈Idl⁡R∧A∈j→x∈X|∃y∈Xx=yHA⊆j
130 129 ex ⊢R∈RingOps∧j∈Idl⁡R→A∈j→x∈X|∃y∈Xx=yHA⊆j
131 120 130 syl5 ⊢R∈RingOps∧j∈Idl⁡R→A∈X∧A⊆j→x∈X|∃y∈Xx=yHA⊆j
132 131 expdimp ⊢R∈RingOps∧j∈Idl⁡R∧A∈X→A⊆j→x∈X|∃y∈Xx=yHA⊆j
133 132 an32s ⊢R∈RingOps∧A∈X∧j∈Idl⁡R→A⊆j→x∈X|∃y∈Xx=yHA⊆j
134 133 ralrimiva ⊢R∈RingOps∧A∈X→∀j∈Idl⁡RA⊆j→x∈X|∃y∈Xx=yHA⊆j
135 4 134 sylan ⊢R∈CRingOps∧A∈X→∀j∈Idl⁡RA⊆j→x∈X|∃y∈Xx=yHA⊆j
136 101 118 135 3jca ⊢R∈CRingOps∧A∈X→x∈X|∃y∈Xx=yHA∈Idl⁡R∧A⊆x∈X|∃y∈Xx=yHA∧∀j∈Idl⁡RA⊆j→x∈X|∃y∈Xx=yHA⊆j
137 snssi ⊢A∈X→A⊆X
138 1 3 igenval2 ⊢R∈RingOps∧A⊆X→RIdlGenA=x∈X|∃y∈Xx=yHA↔x∈X|∃y∈Xx=yHA∈Idl⁡R∧A⊆x∈X|∃y∈Xx=yHA∧∀j∈Idl⁡RA⊆j→x∈X|∃y∈Xx=yHA⊆j
139 4 137 138 syl2an ⊢R∈CRingOps∧A∈X→RIdlGenA=x∈X|∃y∈Xx=yHA↔x∈X|∃y∈Xx=yHA∈Idl⁡R∧A⊆x∈X|∃y∈Xx=yHA∧∀j∈Idl⁡RA⊆j→x∈X|∃y∈Xx=yHA⊆j
140 136 139 mpbird ⊢R∈CRingOps∧A∈X→RIdlGenA=x∈X|∃y∈Xx=yHA