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 36923

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 36856	. . . . 5 ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2		ssrab2 4076	. . . . . . 7 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
3	2	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4		prnc.1	. . . . . . . . 9 ⊢ 𝐺 = (1^st ‘𝑅)
5		prnc.3	. . . . . . . . 9 ⊢ 𝑋 = ran 𝐺
6		eqid 2732	. . . . . . . . 9 ⊢ (GId‘𝐺) = (GId‘𝐺)
7	4, 5, 6	rngo0cl 36775	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
8	7	adantr 481	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ 𝑋)
9		prnc.2	. . . . . . . . . 10 ⊢ 𝐻 = (2^nd ‘𝑅)
10	6, 5, 4, 9	rngolz 36778	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
11	10	eqcomd 2738	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12		oveq1 7412	. . . . . . . . 9 ⊢ (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
13	12	rspceeqv 3632	. . . . . . . 8 ⊢ (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
14	8, 11, 13	syl2anc 584	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15		eqeq1 2736	. . . . . . . . 9 ⊢ (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
16	15	rexbidv 3178	. . . . . . . 8 ⊢ (𝑥 = (GId‘𝐺) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
17	16	elrab 3682	. . . . . . 7 ⊢ ((GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
18	8, 14, 17	sylanbrc 583	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
19		eqeq1 2736	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
20	19	rexbidv 3178	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴)))
21		oveq1 7412	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
22	21	eqeq2d 2743	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
23	22	cbvrexvw 3235	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴))
24	20, 23	bitrdi 286	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
25	24	elrab 3682	. . . . . . . 8 ⊢ (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
26		eqeq1 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
27	26	rexbidv 3178	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴)))
28		oveq1 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
29	28	eqeq2d 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
30	29	cbvrexvw 3235	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴))
31	27, 30	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
32	31	elrab 3682	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
33	4, 9, 5	rngodir 36761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34	33	3exp2 1354	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ RingOps → (𝑟 ∈ 𝑋 → (𝑠 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
35	34	imp42 427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
36	4, 5	rngogcl 36768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37	36	3expib 1122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ RingOps → ((𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
38	37	imdistani 569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
39	4, 9, 5	rngocl 36757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40	39	3expa 1118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
43	42	rspceeqv 3632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
44	41, 43	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
45	44	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46		eqeq1 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
47	46	rexbidv 3178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
48	47	elrab 3682	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
49	40, 45, 48	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
50	38, 49	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
51	35, 50	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
52	51	an32s 650	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
53	52	anassrs 468	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
54		oveq2 7413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
55	54	eleq1d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
56	53, 55	syl5ibrcom 246	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
57	56	rexlimdva 3155	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
58	57	adantld 491	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ((𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
59	32, 58	biimtrid 241	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
60	59	ralrimiv 3145	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
61	4, 9, 5	rngoass 36762	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62	61	3exp2 1354	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → (𝑤 ∈ 𝑋 → (𝑟 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
63	62	imp42 427	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
64	63	an32s 650	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
65	4, 9, 5	rngocl 36757	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66	65	3expib 1122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ RingOps → ((𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
67	66	imdistani 569	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
68	4, 9, 5	rngocl 36757	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69	68	3expa 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70		eqid 2732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71		oveq1 7412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
72	71	rspceeqv 3632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
73	70, 72	mpan2 689	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
74	73	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75		eqeq1 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
76	75	rexbidv 3178	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
77	76	elrab 3682	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
78	69, 74, 77	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
79	67, 78	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
80	79	an32s 650	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
81	64, 80	eqeltrrd 2834	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
82	81	anass1rs 653	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
83	82	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
84	60, 83	jca 512	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
85		oveq1 7412	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
86	85	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
87	86	ralbidv 3177	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
88		oveq2 7413	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
89	88	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
90	89	ralbidv 3177	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
91	87, 90	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
92	84, 91	syl5ibrcom 246	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
93	92	rexlimdva 3155	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
94	93	adantld 491	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
95	25, 94	biimtrid 241	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
96	95	ralrimiv 3145	. . . . . 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 36871	. . . . 5 ⊢ (𝑅 ∈ CRingOps → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))))
100	99	adantr 481	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))))
101	98, 100	mpbird 256	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102		simpr 485	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
103	4	rneqi 5934	. . . . . . . . . 10 ⊢ ran 𝐺 = ran (1^st ‘𝑅)
104	5, 103	eqtri 2760	. . . . . . . . 9 ⊢ 𝑋 = ran (1^st ‘𝑅)
105		eqid 2732	. . . . . . . . 9 ⊢ (GId‘𝐻) = (GId‘𝐻)
106	104, 9, 105	rngo1cl 36795	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107	106	adantr 481	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐻) ∈ 𝑋)
108	9, 104, 105	rngolidm 36793	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109	108	eqcomd 2738	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110		oveq1 7412	. . . . . . . 8 ⊢ (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111	110	rspceeqv 3632	. . . . . . 7 ⊢ (((GId‘𝐻) ∈ 𝑋 ∧ 𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
112	107, 109, 111	syl2anc 584	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
113	1, 112	sylan 580	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
114		eqeq1 2736	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115	114	rexbidv 3178	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
116	115	elrab 3682	. . . . 5 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
117	102, 113, 116	sylanbrc 583	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
118	117	snssd 4811	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
119		snssg 4786	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑗 ↔ {𝐴} ⊆ 𝑗))
120	119	biimpar 478	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴 ∈ 𝑗)
121	4, 9, 5	idllmulcl 36876	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝑗 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122	121	anassrs 468	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123		eleq1 2821	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦𝐻𝐴) → (𝑥 ∈ 𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124	122, 123	syl5ibrcom 246	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
125	124	rexlimdva 3155	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
126	125	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
127	126	ralrimiva 3146	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
128		rabss 4068	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
129	127, 128	sylibr 233	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
130	129	ex 413	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴 ∈ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
131	120, 130	syl5 34	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
132	131	expdimp 453	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
133	132	an32s 650	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134	133	ralrimiva 3146	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
135	1, 134	sylan 580	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136	101, 118, 135	3jca 1128	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137		snssi 4810	. . 3 ⊢ (𝐴 ∈ 𝑋 → {𝐴} ⊆ 𝑋)
138	4, 5	igenval2 36922	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
139	1, 137, 138	syl2an 596	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
140	136, 139	mpbird 256	1 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 ∃wrex 3070 {crab 3432 ⊆ wss 3947 {csn 4627 ran crn 5676 ‘cfv 6540 (class class class)co 7405 1^st c1st 7969 2^nd c2nd 7970 GIdcgi 29730 RingOpscrngo 36750 CRingOpsccring 36849 Idlcidl 36863 IdlGen cigen 36915

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7971 df-2nd 7972 df-grpo 29733 df-gid 29734 df-ginv 29735 df-ablo 29785 df-ass 36699 df-exid 36701 df-mgmOLD 36705 df-sgrOLD 36717 df-mndo 36723 df-rngo 36751 df-com2 36846 df-crngo 36850 df-idl 36866 df-igen 36916

This theorem is referenced by: isfldidl 36924 ispridlc 36926

W3C validator