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 = 1 st R
prnc.2 H = 2 nd R
prnc.3 X = ran G
Assertion prnc R CRingOps A X R IdlGen A = x X | y X x = y H A

Proof

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