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 e. CRingOps /\ A e. X ) -> ( R IdlGen { A } ) = { x e. X | E. y e. X x = ( y H A ) } )

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