This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
prnc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
prnc.3 ⊢ 𝑋 = ran 𝐺
Assertion prnc ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝐴 } ) = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )

Proof

Step Hyp Ref Expression
1 prnc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 prnc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 prnc.3 ⊢ 𝑋 = ran 𝐺
4 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
5 ssrab2 ⊢ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑋
6 5 a1i ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑋 )
7 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
8 1 3 7 rngo0cl ⊢ ( 𝑅 ∈ RingOps → ( GId ‘ 𝐺 ) ∈ 𝑋 )
9 8 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( GId ‘ 𝐺 ) ∈ 𝑋 )
10 7 3 1 2 rngolz ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐻 𝐴 ) = ( GId ‘ 𝐺 ) )
11 10 eqcomd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( GId ‘ 𝐺 ) = ( ( GId ‘ 𝐺 ) 𝐻 𝐴 ) )
12 oveq1 ⊢ ( 𝑦 = ( GId ‘ 𝐺 ) → ( 𝑦 𝐻 𝐴 ) = ( ( GId ‘ 𝐺 ) 𝐻 𝐴 ) )
13 12 rspceeqv ⊢ ( ( ( GId ‘ 𝐺 ) ∈ 𝑋 ∧ ( GId ‘ 𝐺 ) = ( ( GId ‘ 𝐺 ) 𝐻 𝐴 ) ) → ∃ 𝑦 ∈ 𝑋 ( GId ‘ 𝐺 ) = ( 𝑦 𝐻 𝐴 ) )
14 9 11 13 syl2anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( GId ‘ 𝐺 ) = ( 𝑦 𝐻 𝐴 ) )
15 eqeq1 ⊢ ( 𝑥 = ( GId ‘ 𝐺 ) → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ( GId ‘ 𝐺 ) = ( 𝑦 𝐻 𝐴 ) ) )
16 15 rexbidv ⊢ ( 𝑥 = ( GId ‘ 𝐺 ) → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 ( GId ‘ 𝐺 ) = ( 𝑦 𝐻 𝐴 ) ) )
17 16 elrab ⊢ ( ( GId ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( ( GId ‘ 𝐺 ) ∈ 𝑋 ∧ ∃ 𝑦 ∈ 𝑋 ( GId ‘ 𝐺 ) = ( 𝑦 𝐻 𝐴 ) ) )
18 9 14 17 sylanbrc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( GId ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
19 eqeq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ 𝑢 = ( 𝑦 𝐻 𝐴 ) ) )
20 19 rexbidv ⊢ ( 𝑥 = 𝑢 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 𝑢 = ( 𝑦 𝐻 𝐴 ) ) )
21 oveq1 ⊢ ( 𝑦 = 𝑟 → ( 𝑦 𝐻 𝐴 ) = ( 𝑟 𝐻 𝐴 ) )
22 21 eqeq2d ⊢ ( 𝑦 = 𝑟 → ( 𝑢 = ( 𝑦 𝐻 𝐴 ) ↔ 𝑢 = ( 𝑟 𝐻 𝐴 ) ) )
23 22 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑋 𝑢 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑟 ∈ 𝑋 𝑢 = ( 𝑟 𝐻 𝐴 ) )
24 20 23 bitrdi ⊢ ( 𝑥 = 𝑢 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑟 ∈ 𝑋 𝑢 = ( 𝑟 𝐻 𝐴 ) ) )
25 24 elrab ⊢ ( 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( 𝑢 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑢 = ( 𝑟 𝐻 𝐴 ) ) )
26 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ 𝑣 = ( 𝑦 𝐻 𝐴 ) ) )
27 26 rexbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 𝐻 𝐴 ) ) )
28 oveq1 ⊢ ( 𝑦 = 𝑠 → ( 𝑦 𝐻 𝐴 ) = ( 𝑠 𝐻 𝐴 ) )
29 28 eqeq2d ⊢ ( 𝑦 = 𝑠 → ( 𝑣 = ( 𝑦 𝐻 𝐴 ) ↔ 𝑣 = ( 𝑠 𝐻 𝐴 ) ) )
30 29 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑋 𝑣 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑠 ∈ 𝑋 𝑣 = ( 𝑠 𝐻 𝐴 ) )
31 27 30 bitrdi ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑠 ∈ 𝑋 𝑣 = ( 𝑠 𝐻 𝐴 ) ) )
32 31 elrab ⊢ ( 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( 𝑣 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑣 = ( 𝑠 𝐻 𝐴 ) ) )
33 1 2 3 rngodir ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) )
34 33 3exp2 ⊢ ( 𝑅 ∈ RingOps → ( 𝑟 ∈ 𝑋 → ( 𝑠 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) ) ) ) )
35 34 imp42 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) )
36 1 3 rngogcl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 )
37 36 3expib ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ) )
38 37 imdistani ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( 𝑅 ∈ RingOps ∧ ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ) )
39 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ∈ 𝑋 )
40 39 3expa ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ∈ 𝑋 )
41 eqid ⊢ ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 )
42 oveq1 ⊢ ( 𝑦 = ( 𝑟 𝐺 𝑠 ) → ( 𝑦 𝐻 𝐴 ) = ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) )
43 42 rspceeqv ⊢ ( ( ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ∧ ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) )
44 41 43 mpan2 ⊢ ( ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 → ∃ 𝑦 ∈ 𝑋 ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) )
45 44 ad2antlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) )
46 eqeq1 ⊢ ( 𝑥 = ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) ) )
47 46 rexbidv ⊢ ( 𝑥 = ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) ) )
48 47 elrab ⊢ ( ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ∈ 𝑋 ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) ) )
49 40 45 48 sylanbrc ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 𝐺 𝑠 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
50 38 49 sylan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑟 𝐺 𝑠 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
51 35 50 eqeltrrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
52 51 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
53 52 anassrs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
54 oveq2 ⊢ ( 𝑣 = ( 𝑠 𝐻 𝐴 ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) = ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) )
55 54 eleq1d ⊢ ( 𝑣 = ( 𝑠 𝐻 𝐴 ) → ( ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( ( 𝑟 𝐻 𝐴 ) 𝐺 ( 𝑠 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
56 53 55 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝑋 ) → ( 𝑣 = ( 𝑠 𝐻 𝐴 ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
57 56 rexlimdva ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ( ∃ 𝑠 ∈ 𝑋 𝑣 = ( 𝑠 𝐻 𝐴 ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
58 57 adantld ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ( ( 𝑣 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑣 = ( 𝑠 𝐻 𝐴 ) ) → ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
59 32 58 biimtrid ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ( 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } → ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
60 59 ralrimiv ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
61 1 2 3 rngoass ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) )
62 61 3exp2 ⊢ ( 𝑅 ∈ RingOps → ( 𝑤 ∈ 𝑋 → ( 𝑟 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ) ) ) )
63 62 imp42 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) )
64 63 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) )
65 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) → ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 )
66 65 3expib ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) → ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ) )
67 66 imdistani ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) → ( 𝑅 ∈ RingOps ∧ ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ) )
68 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ 𝑋 )
69 68 3expa ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ 𝑋 )
70 eqid ⊢ ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 )
71 oveq1 ⊢ ( 𝑦 = ( 𝑤 𝐻 𝑟 ) → ( 𝑦 𝐻 𝐴 ) = ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) )
72 71 rspceeqv ⊢ ( ( ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ∧ ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) )
73 70 72 mpan2 ⊢ ( ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 → ∃ 𝑦 ∈ 𝑋 ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) )
74 73 ad2antlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) )
75 eqeq1 ⊢ ( 𝑥 = ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) ) )
76 75 rexbidv ⊢ ( 𝑥 = ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) ) )
77 76 elrab ⊢ ( ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ 𝑋 ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) = ( 𝑦 𝐻 𝐴 ) ) )
78 69 74 77 sylanbrc ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 𝐻 𝑟 ) ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
79 67 78 sylan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
80 79 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) → ( ( 𝑤 𝐻 𝑟 ) 𝐻 𝐴 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
81 64 80 eqeltrrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ) ) → ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
82 81 anass1rs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
83 82 ralrimiva ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
84 60 83 jca ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
85 oveq1 ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( 𝑢 𝐺 𝑣 ) = ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) )
86 85 eleq1d ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
87 86 ralbidv ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
88 oveq2 ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( 𝑤 𝐻 𝑢 ) = ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) )
89 88 eleq1d ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
90 89 ralbidv ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
91 87 90 anbi12d ⊢ ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ↔ ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ( 𝑟 𝐻 𝐴 ) 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 ( 𝑟 𝐻 𝐴 ) ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
92 84 91 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ 𝑋 ) → ( 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
93 92 rexlimdva ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ 𝑋 𝑢 = ( 𝑟 𝐻 𝐴 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
94 93 adantld ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑢 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑢 = ( 𝑟 𝐻 𝐴 ) ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
95 25 94 biimtrid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
96 95 ralrimiv ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) )
97 6 18 96 3jca ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
98 4 97 sylan ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) )
99 1 2 3 7 isidlc ⊢ ( 𝑅 ∈ CRingOps → ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∈ ( Idl ‘ 𝑅 ) ↔ ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) ) )
100 99 adantr ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∈ ( Idl ‘ 𝑅 ) ↔ ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑢 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ( 𝑢 𝐺 𝑣 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑤 ∈ 𝑋 ( 𝑤 𝐻 𝑢 ) ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ) ) ) )
101 98 100 mpbird ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∈ ( Idl ‘ 𝑅 ) )
102 simpr ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
103 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
104 3 103 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
105 eqid ⊢ ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
106 104 2 105 rngo1cl ⊢ ( 𝑅 ∈ RingOps → ( GId ‘ 𝐻 ) ∈ 𝑋 )
107 106 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( GId ‘ 𝐻 ) ∈ 𝑋 )
108 2 104 105 rngolidm ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( GId ‘ 𝐻 ) 𝐻 𝐴 ) = 𝐴 )
109 108 eqcomd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → 𝐴 = ( ( GId ‘ 𝐻 ) 𝐻 𝐴 ) )
110 oveq1 ⊢ ( 𝑦 = ( GId ‘ 𝐻 ) → ( 𝑦 𝐻 𝐴 ) = ( ( GId ‘ 𝐻 ) 𝐻 𝐴 ) )
111 110 rspceeqv ⊢ ( ( ( GId ‘ 𝐻 ) ∈ 𝑋 ∧ 𝐴 = ( ( GId ‘ 𝐻 ) 𝐻 𝐴 ) ) → ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 𝐻 𝐴 ) )
112 107 109 111 syl2anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 𝐻 𝐴 ) )
113 4 112 sylan ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 𝐻 𝐴 ) )
114 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ 𝐴 = ( 𝑦 𝐻 𝐴 ) ) )
115 114 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 𝐻 𝐴 ) ) )
116 115 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( 𝐴 ∈ 𝑋 ∧ ∃ 𝑦 ∈ 𝑋 𝐴 = ( 𝑦 𝐻 𝐴 ) ) )
117 102 113 116 sylanbrc ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
118 117 snssd ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ⊆ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )
119 snssg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ 𝑗 ↔ { 𝐴 } ⊆ 𝑗 ) )
120 119 biimpar ⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝐴 } ⊆ 𝑗 ) → 𝐴 ∈ 𝑗 )
121 1 2 3 idllmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝑗 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 𝐻 𝐴 ) ∈ 𝑗 )
122 121 anassrs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑗 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝐻 𝐴 ) ∈ 𝑗 )
123 eleq1 ⊢ ( 𝑥 = ( 𝑦 𝐻 𝐴 ) → ( 𝑥 ∈ 𝑗 ↔ ( 𝑦 𝐻 𝐴 ) ∈ 𝑗 ) )
124 122 123 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑗 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 = ( 𝑦 𝐻 𝐴 ) → 𝑥 ∈ 𝑗 ) )
125 124 rexlimdva ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑗 ) → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) → 𝑥 ∈ 𝑗 ) )
126 125 adantr ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑗 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) → 𝑥 ∈ 𝑗 ) )
127 126 ralrimiva ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑗 ) → ∀ 𝑥 ∈ 𝑋 ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) → 𝑥 ∈ 𝑗 ) )
128 rabss ⊢ ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ↔ ∀ 𝑥 ∈ 𝑋 ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) → 𝑥 ∈ 𝑗 ) )
129 127 128 sylibr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑗 ) → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 )
130 129 ex ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐴 ∈ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) )
131 120 130 syl5 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ { 𝐴 } ⊆ 𝑗 ) → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) )
132 131 expdimp ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) )
133 132 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) → ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) )
134 133 ralrimiva ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) )
135 4 134 sylan ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) )
136 101 118 135 3jca ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝐴 } ⊆ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) ) )
137 snssi ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ⊆ 𝑋 )
138 1 3 igenval2 ⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝐴 } ⊆ 𝑋 ) → ( ( 𝑅 IdlGen { 𝐴 } ) = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝐴 } ⊆ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) ) ) )
139 4 137 138 syl2an ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑅 IdlGen { 𝐴 } ) = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ↔ ( { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝐴 } ⊆ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( { 𝐴 } ⊆ 𝑗 → { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } ⊆ 𝑗 ) ) ) )
140 136 139 mpbird ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝐴 } ) = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 𝐻 𝐴 ) } )