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 38388

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 38321	. . . . 5 ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2		ssrab2 4020	. . . . . . 7 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
3	2	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4		prnc.1	. . . . . . . . 9 ⊢ 𝐺 = (1^st ‘𝑅)
5		prnc.3	. . . . . . . . 9 ⊢ 𝑋 = ran 𝐺
6		eqid 2736	. . . . . . . . 9 ⊢ (GId‘𝐺) = (GId‘𝐺)
7	4, 5, 6	rngo0cl 38240	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
8	7	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ 𝑋)
9		prnc.2	. . . . . . . . . 10 ⊢ 𝐻 = (2^nd ‘𝑅)
10	6, 5, 4, 9	rngolz 38243	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
11	10	eqcomd 2742	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12		oveq1 7374	. . . . . . . . 9 ⊢ (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
13	12	rspceeqv 3587	. . . . . . . 8 ⊢ (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
14	8, 11, 13	syl2anc 585	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
16	15	rexbidv 3161	. . . . . . . 8 ⊢ (𝑥 = (GId‘𝐺) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
17	16	elrab 3634	. . . . . . 7 ⊢ ((GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
18	8, 14, 17	sylanbrc 584	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
19		eqeq1 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
20	19	rexbidv 3161	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴)))
21		oveq1 7374	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
22	21	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
23	22	cbvrexvw 3216	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴))
24	20, 23	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
25	24	elrab 3634	. . . . . . . 8 ⊢ (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
26		eqeq1 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
27	26	rexbidv 3161	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴)))
28		oveq1 7374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
29	28	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
30	29	cbvrexvw 3216	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴))
31	27, 30	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
32	31	elrab 3634	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
33	4, 9, 5	rngodir 38226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34	33	3exp2 1356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ RingOps → (𝑟 ∈ 𝑋 → (𝑠 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
35	34	imp42 426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
36	4, 5	rngogcl 38233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37	36	3expib 1123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ RingOps → ((𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
38	37	imdistani 568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
39	4, 9, 5	rngocl 38222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40	39	3expa 1119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
43	42	rspceeqv 3587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
44	41, 43	mpan2 692	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
45	44	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
47	46	rexbidv 3161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
48	47	elrab 3634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
49	40, 45, 48	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
50	38, 49	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
51	35, 50	eqeltrrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
52	51	an32s 653	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
53	52	anassrs 467	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
54		oveq2 7375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
55	54	eleq1d 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
56	53, 55	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
57	56	rexlimdva 3138	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
58	57	adantld 490	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ((𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
59	32, 58	biimtrid 242	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
60	59	ralrimiv 3128	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
61	4, 9, 5	rngoass 38227	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62	61	3exp2 1356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → (𝑤 ∈ 𝑋 → (𝑟 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
63	62	imp42 426	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
64	63	an32s 653	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
65	4, 9, 5	rngocl 38222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66	65	3expib 1123	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ RingOps → ((𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
67	66	imdistani 568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
68	4, 9, 5	rngocl 38222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69	68	3expa 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71		oveq1 7374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
72	71	rspceeqv 3587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
73	70, 72	mpan2 692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
74	73	ad2antlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75		eqeq1 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
76	75	rexbidv 3161	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
77	76	elrab 3634	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
78	69, 74, 77	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
79	67, 78	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
80	79	an32s 653	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
81	64, 80	eqeltrrd 2837	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
82	81	anass1rs 656	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
83	82	ralrimiva 3129	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
84	60, 83	jca 511	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
85		oveq1 7374	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
86	85	eleq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
87	86	ralbidv 3160	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
88		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
89	88	eleq1d 2821	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
90	89	ralbidv 3160	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
91	87, 90	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
92	84, 91	syl5ibrcom 247	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
93	92	rexlimdva 3138	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
94	93	adantld 490	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
95	25, 94	biimtrid 242	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
96	95	ralrimiv 3128	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
97	3, 18, 96	3jca 1129	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
98	1, 97	sylan 581	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
99	4, 9, 5, 6	isidlc 38336	. . . . 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 5892	. . . . . . . . . 10 ⊢ ran 𝐺 = ran (1^st ‘𝑅)
104	5, 103	eqtri 2759	. . . . . . . . 9 ⊢ 𝑋 = ran (1^st ‘𝑅)
105		eqid 2736	. . . . . . . . 9 ⊢ (GId‘𝐻) = (GId‘𝐻)
106	104, 9, 105	rngo1cl 38260	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107	106	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐻) ∈ 𝑋)
108	9, 104, 105	rngolidm 38258	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109	108	eqcomd 2742	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110		oveq1 7374	. . . . . . . 8 ⊢ (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111	110	rspceeqv 3587	. . . . . . 7 ⊢ (((GId‘𝐻) ∈ 𝑋 ∧ 𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
112	107, 109, 111	syl2anc 585	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
113	1, 112	sylan 581	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
114		eqeq1 2740	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115	114	rexbidv 3161	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
116	115	elrab 3634	. . . . 5 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
117	102, 113, 116	sylanbrc 584	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
118	117	snssd 4730	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
119		snssg 4727	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑗 ↔ {𝐴} ⊆ 𝑗))
120	119	biimpar 477	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴 ∈ 𝑗)
121	4, 9, 5	idllmulcl 38341	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝑗 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122	121	anassrs 467	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123		eleq1 2824	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦𝐻𝐴) → (𝑥 ∈ 𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124	122, 123	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
125	124	rexlimdva 3138	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
126	125	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
127	126	ralrimiva 3129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
128		rabss 4010	. . . . . . . . . 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 653	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134	133	ralrimiva 3129	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
135	1, 134	sylan 581	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136	101, 118, 135	3jca 1129	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137		snssi 4729	. . 3 ⊢ (𝐴 ∈ 𝑋 → {𝐴} ⊆ 𝑋)
138	4, 5	igenval2 38387	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
139	1, 137, 138	syl2an 597	. 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 1542 ∈ wcel 2114 ∀wral 3051 ∃wrex 3061 {crab 3389 ⊆ wss 3889 {csn 4567 ran crn 5632 ‘cfv 6498 (class class class)co 7367 1^st c1st 7940 2^nd c2nd 7941 GIdcgi 30561 RingOpscrngo 38215 CRingOpsccring 38314 Idlcidl 38328 IdlGen cigen 38380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-1st 7942 df-2nd 7943 df-grpo 30564 df-gid 30565 df-ginv 30566 df-ablo 30616 df-ass 38164 df-exid 38166 df-mgmOLD 38170 df-sgrOLD 38182 df-mndo 38188 df-rngo 38216 df-com2 38311 df-crngo 38315 df-idl 38331 df-igen 38381

This theorem is referenced by: isfldidl 38389 ispridlc 38391

W3C validator