prnc - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > prnc		Structured version Visualization version GIF version

Theorem prnc 38027

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

**Hypotheses**
Ref	Expression
prnc.1	⊢ 𝐺 = (1^st ‘𝑅)
prnc.2	⊢ 𝐻 = (2^nd ‘𝑅)
prnc.3	⊢ 𝑋 = ran 𝐺

**Assertion**
Ref	Expression
prnc	⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})

Distinct variable groups: 𝑥,𝑅,𝑦 𝑥,𝑋,𝑦 𝑥,𝐺,𝑦 𝑥,𝐻,𝑦 𝑥,𝐴,𝑦

Proof of Theorem prnc Dummy variables 𝑗 𝑢 𝑣 𝑤 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		crngorngo 37960	. . . . 5 ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2		ssrab2 4103	. . . . . . 7 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
3	2	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4		prnc.1	. . . . . . . . 9 ⊢ 𝐺 = (1^st ‘𝑅)
5		prnc.3	. . . . . . . . 9 ⊢ 𝑋 = ran 𝐺
6		eqid 2740	. . . . . . . . 9 ⊢ (GId‘𝐺) = (GId‘𝐺)
7	4, 5, 6	rngo0cl 37879	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
8	7	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ 𝑋)
9		prnc.2	. . . . . . . . . 10 ⊢ 𝐻 = (2^nd ‘𝑅)
10	6, 5, 4, 9	rngolz 37882	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
11	10	eqcomd 2746	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12		oveq1 7455	. . . . . . . . 9 ⊢ (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
13	12	rspceeqv 3658	. . . . . . . 8 ⊢ (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
14	8, 11, 13	syl2anc 583	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15		eqeq1 2744	. . . . . . . . 9 ⊢ (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
16	15	rexbidv 3185	. . . . . . . 8 ⊢ (𝑥 = (GId‘𝐺) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
17	16	elrab 3708	. . . . . . 7 ⊢ ((GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
18	8, 14, 17	sylanbrc 582	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
19		eqeq1 2744	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
20	19	rexbidv 3185	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴)))
21		oveq1 7455	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
22	21	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
23	22	cbvrexvw 3244	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴))
24	20, 23	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
25	24	elrab 3708	. . . . . . . 8 ⊢ (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
26		eqeq1 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
27	26	rexbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴)))
28		oveq1 7455	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
29	28	eqeq2d 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
30	29	cbvrexvw 3244	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴))
31	27, 30	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
32	31	elrab 3708	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
33	4, 9, 5	rngodir 37865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34	33	3exp2 1354	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ RingOps → (𝑟 ∈ 𝑋 → (𝑠 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
35	34	imp42 426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
36	4, 5	rngogcl 37872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37	36	3expib 1122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ RingOps → ((𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
38	37	imdistani 568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
39	4, 9, 5	rngocl 37861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40	39	3expa 1118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
43	42	rspceeqv 3658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
44	41, 43	mpan2 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
45	44	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
47	46	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
48	47	elrab 3708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
49	40, 45, 48	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
50	38, 49	sylan 579	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
51	35, 50	eqeltrrd 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
52	51	an32s 651	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
53	52	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
54		oveq2 7456	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
55	54	eleq1d 2829	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
56	53, 55	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
57	56	rexlimdva 3161	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
58	57	adantld 490	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ((𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
59	32, 58	biimtrid 242	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
60	59	ralrimiv 3151	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
61	4, 9, 5	rngoass 37866	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62	61	3exp2 1354	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → (𝑤 ∈ 𝑋 → (𝑟 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
63	62	imp42 426	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
64	63	an32s 651	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
65	4, 9, 5	rngocl 37861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66	65	3expib 1122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ RingOps → ((𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
67	66	imdistani 568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
68	4, 9, 5	rngocl 37861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69	68	3expa 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71		oveq1 7455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
72	71	rspceeqv 3658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
73	70, 72	mpan2 690	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
74	73	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75		eqeq1 2744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
76	75	rexbidv 3185	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
77	76	elrab 3708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
78	69, 74, 77	sylanbrc 582	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
79	67, 78	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
80	79	an32s 651	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
81	64, 80	eqeltrrd 2845	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
82	81	anass1rs 654	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
83	82	ralrimiva 3152	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
84	60, 83	jca 511	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
85		oveq1 7455	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
86	85	eleq1d 2829	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
87	86	ralbidv 3184	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
88		oveq2 7456	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
89	88	eleq1d 2829	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
90	89	ralbidv 3184	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
91	87, 90	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
92	84, 91	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
93	92	rexlimdva 3161	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
94	93	adantld 490	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
95	25, 94	biimtrid 242	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
96	95	ralrimiv 3151	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
97	3, 18, 96	3jca 1128	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
98	1, 97	sylan 579	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
99	4, 9, 5, 6	isidlc 37975	. . . . 5 ⊢ (𝑅 ∈ CRingOps → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))))
100	99	adantr 480	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))))
101	98, 100	mpbird 257	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102		simpr 484	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
103	4	rneqi 5962	. . . . . . . . . 10 ⊢ ran 𝐺 = ran (1^st ‘𝑅)
104	5, 103	eqtri 2768	. . . . . . . . 9 ⊢ 𝑋 = ran (1^st ‘𝑅)
105		eqid 2740	. . . . . . . . 9 ⊢ (GId‘𝐻) = (GId‘𝐻)
106	104, 9, 105	rngo1cl 37899	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107	106	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐻) ∈ 𝑋)
108	9, 104, 105	rngolidm 37897	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109	108	eqcomd 2746	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110		oveq1 7455	. . . . . . . 8 ⊢ (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111	110	rspceeqv 3658	. . . . . . 7 ⊢ (((GId‘𝐻) ∈ 𝑋 ∧ 𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
112	107, 109, 111	syl2anc 583	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
113	1, 112	sylan 579	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
114		eqeq1 2744	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115	114	rexbidv 3185	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
116	115	elrab 3708	. . . . 5 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
117	102, 113, 116	sylanbrc 582	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
118	117	snssd 4834	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
119		snssg 4808	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑗 ↔ {𝐴} ⊆ 𝑗))
120	119	biimpar 477	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴 ∈ 𝑗)
121	4, 9, 5	idllmulcl 37980	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝑗 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122	121	anassrs 467	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123		eleq1 2832	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦𝐻𝐴) → (𝑥 ∈ 𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124	122, 123	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
125	124	rexlimdva 3161	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
126	125	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
127	126	ralrimiva 3152	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
128		rabss 4095	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
129	127, 128	sylibr 234	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
130	129	ex 412	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴 ∈ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
131	120, 130	syl5 34	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
132	131	expdimp 452	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
133	132	an32s 651	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134	133	ralrimiva 3152	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
135	1, 134	sylan 579	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136	101, 118, 135	3jca 1128	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137		snssi 4833	. . 3 ⊢ (𝐴 ∈ 𝑋 → {𝐴} ⊆ 𝑋)
138	4, 5	igenval2 38026	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
139	1, 137, 138	syl2an 595	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
140	136, 139	mpbird 257	1 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 {crab 3443 ⊆ wss 3976 {csn 4648 ran crn 5701 ‘cfv 6573 (class class class)co 7448 1^st c1st 8028 2^nd c2nd 8029 GIdcgi 30522 RingOpscrngo 37854 CRingOpsccring 37953 Idlcidl 37967 IdlGen cigen 38019

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031 df-grpo 30525 df-gid 30526 df-ginv 30527 df-ablo 30577 df-ass 37803 df-exid 37805 df-mgmOLD 37809 df-sgrOLD 37821 df-mndo 37827 df-rngo 37855 df-com2 37950 df-crngo 37954 df-idl 37970 df-igen 38020

This theorem is referenced by: isfldidl 38028 ispridlc 38030

W3C validator