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 38047

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 37980	. . . . 5 ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2		ssrab2 4031	. . . . . . 7 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
3	2	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4		prnc.1	. . . . . . . . 9 ⊢ 𝐺 = (1^st ‘𝑅)
5		prnc.3	. . . . . . . . 9 ⊢ 𝑋 = ran 𝐺
6		eqid 2729	. . . . . . . . 9 ⊢ (GId‘𝐺) = (GId‘𝐺)
7	4, 5, 6	rngo0cl 37899	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
8	7	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ 𝑋)
9		prnc.2	. . . . . . . . . 10 ⊢ 𝐻 = (2^nd ‘𝑅)
10	6, 5, 4, 9	rngolz 37902	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
11	10	eqcomd 2735	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12		oveq1 7356	. . . . . . . . 9 ⊢ (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
13	12	rspceeqv 3600	. . . . . . . 8 ⊢ (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
14	8, 11, 13	syl2anc 584	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15		eqeq1 2733	. . . . . . . . 9 ⊢ (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
16	15	rexbidv 3153	. . . . . . . 8 ⊢ (𝑥 = (GId‘𝐺) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
17	16	elrab 3648	. . . . . . 7 ⊢ ((GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
18	8, 14, 17	sylanbrc 583	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
19		eqeq1 2733	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
20	19	rexbidv 3153	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴)))
21		oveq1 7356	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
22	21	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
23	22	cbvrexvw 3208	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴))
24	20, 23	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
25	24	elrab 3648	. . . . . . . 8 ⊢ (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
26		eqeq1 2733	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
27	26	rexbidv 3153	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴)))
28		oveq1 7356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
29	28	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
30	29	cbvrexvw 3208	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴))
31	27, 30	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
32	31	elrab 3648	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
33	4, 9, 5	rngodir 37885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34	33	3exp2 1355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ RingOps → (𝑟 ∈ 𝑋 → (𝑠 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
35	34	imp42 426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
36	4, 5	rngogcl 37892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37	36	3expib 1122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ RingOps → ((𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
38	37	imdistani 568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
39	4, 9, 5	rngocl 37881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40	39	3expa 1118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42		oveq1 7356	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
43	42	rspceeqv 3600	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
44	41, 43	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
45	44	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46		eqeq1 2733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
47	46	rexbidv 3153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
48	47	elrab 3648	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
49	40, 45, 48	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
50	38, 49	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
51	35, 50	eqeltrrd 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
52	51	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
53	52	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
54		oveq2 7357	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
55	54	eleq1d 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
56	53, 55	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
57	56	rexlimdva 3130	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
58	57	adantld 490	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ((𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
59	32, 58	biimtrid 242	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
60	59	ralrimiv 3120	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
61	4, 9, 5	rngoass 37886	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62	61	3exp2 1355	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → (𝑤 ∈ 𝑋 → (𝑟 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
63	62	imp42 426	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
64	63	an32s 652	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
65	4, 9, 5	rngocl 37881	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66	65	3expib 1122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ RingOps → ((𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
67	66	imdistani 568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
68	4, 9, 5	rngocl 37881	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69	68	3expa 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71		oveq1 7356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
72	71	rspceeqv 3600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
73	70, 72	mpan2 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
74	73	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75		eqeq1 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
76	75	rexbidv 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
77	76	elrab 3648	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
78	69, 74, 77	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
79	67, 78	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
80	79	an32s 652	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
81	64, 80	eqeltrrd 2829	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
82	81	anass1rs 655	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
83	82	ralrimiva 3121	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
84	60, 83	jca 511	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
85		oveq1 7356	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
86	85	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
87	86	ralbidv 3152	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
88		oveq2 7357	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
89	88	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
90	89	ralbidv 3152	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
91	87, 90	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
92	84, 91	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
93	92	rexlimdva 3130	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
94	93	adantld 490	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
95	25, 94	biimtrid 242	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
96	95	ralrimiv 3120	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
97	3, 18, 96	3jca 1128	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
98	1, 97	sylan 580	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
99	4, 9, 5, 6	isidlc 37995	. . . . 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 5879	. . . . . . . . . 10 ⊢ ran 𝐺 = ran (1^st ‘𝑅)
104	5, 103	eqtri 2752	. . . . . . . . 9 ⊢ 𝑋 = ran (1^st ‘𝑅)
105		eqid 2729	. . . . . . . . 9 ⊢ (GId‘𝐻) = (GId‘𝐻)
106	104, 9, 105	rngo1cl 37919	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107	106	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐻) ∈ 𝑋)
108	9, 104, 105	rngolidm 37917	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109	108	eqcomd 2735	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110		oveq1 7356	. . . . . . . 8 ⊢ (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111	110	rspceeqv 3600	. . . . . . 7 ⊢ (((GId‘𝐻) ∈ 𝑋 ∧ 𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
112	107, 109, 111	syl2anc 584	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
113	1, 112	sylan 580	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
114		eqeq1 2733	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115	114	rexbidv 3153	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
116	115	elrab 3648	. . . . 5 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
117	102, 113, 116	sylanbrc 583	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
118	117	snssd 4760	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
119		snssg 4735	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑗 ↔ {𝐴} ⊆ 𝑗))
120	119	biimpar 477	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴 ∈ 𝑗)
121	4, 9, 5	idllmulcl 38000	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝑗 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122	121	anassrs 467	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦𝐻𝐴) → (𝑥 ∈ 𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124	122, 123	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
125	124	rexlimdva 3130	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
126	125	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
127	126	ralrimiva 3121	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
128		rabss 4023	. . . . . . . . . 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 652	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134	133	ralrimiva 3121	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
135	1, 134	sylan 580	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136	101, 118, 135	3jca 1128	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137		snssi 4759	. . 3 ⊢ (𝐴 ∈ 𝑋 → {𝐴} ⊆ 𝑋)
138	4, 5	igenval2 38046	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
139	1, 137, 138	syl2an 596	. 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 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 {crab 3394 ⊆ wss 3903 {csn 4577 ran crn 5620 ‘cfv 6482 (class class class)co 7349 1^st c1st 7922 2^nd c2nd 7923 GIdcgi 30434 RingOpscrngo 37874 CRingOpsccring 37973 Idlcidl 37987 IdlGen cigen 38039

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-1st 7924 df-2nd 7925 df-grpo 30437 df-gid 30438 df-ginv 30439 df-ablo 30489 df-ass 37823 df-exid 37825 df-mgmOLD 37829 df-sgrOLD 37841 df-mndo 37847 df-rngo 37875 df-com2 37970 df-crngo 37974 df-idl 37990 df-igen 38040

This theorem is referenced by: isfldidl 38048 ispridlc 38050

W3C validator