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 33866

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 33799	. . . . 5 ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2		ssrab2 3687	. . . . . . 7 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
3	2	a1i 11	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4		prnc.1	. . . . . . . . 9 ⊢ 𝐺 = (1^st ‘𝑅)
5		prnc.3	. . . . . . . . 9 ⊢ 𝑋 = ran 𝐺
6		eqid 2622	. . . . . . . . 9 ⊢ (GId‘𝐺) = (GId‘𝐺)
7	4, 5, 6	rngo0cl 33718	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
8	7	adantr 481	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ 𝑋)
9		prnc.2	. . . . . . . . . 10 ⊢ 𝐻 = (2^nd ‘𝑅)
10	6, 5, 4, 9	rngolz 33721	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
11	10	eqcomd 2628	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
13	12	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑦 = (GId‘𝐺) → ((GId‘𝐺) = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)))
14	13	rspcev 3309	. . . . . . . 8 ⊢ (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15	8, 11, 14	syl2anc 693	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
16		eqeq1 2626	. . . . . . . . 9 ⊢ (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
17	16	rexbidv 3052	. . . . . . . 8 ⊢ (𝑥 = (GId‘𝐺) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
18	17	elrab 3363	. . . . . . 7 ⊢ ((GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
19	8, 15, 18	sylanbrc 698	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
20		eqeq1 2626	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
21	20	rexbidv 3052	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴)))
22		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
23	22	eqeq2d 2632	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
24	23	cbvrexv 3172	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴))
25	21, 24	syl6bb 276	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
26	25	elrab 3363	. . . . . . . 8 ⊢ (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)))
27		eqeq1 2626	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
28	27	rexbidv 3052	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴)))
29		oveq1 6657	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
30	29	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
31	30	cbvrexv 3172	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦 ∈ 𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴))
32	28, 31	syl6bb 276	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑣 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
33	32	elrab 3363	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)))
34	4, 9, 5	rngodir 33704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
35	34	3exp2 1285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 ∈ RingOps → (𝑟 ∈ 𝑋 → (𝑠 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
36	35	imp42 620	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
37	4, 5	rngogcl 33711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
38	37	3expib 1268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ RingOps → ((𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
39	38	imdistani 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
40	4, 9, 5	rngocl 33700	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41	40	3expa 1265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
42		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
43		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
44	43	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑟𝐺𝑠) → (((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)))
45	44	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46	42, 45	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
47	46	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
48		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
49	48	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
50	49	elrab 3363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
51	41, 47, 50	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
52	39, 51	sylan 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
53	36, 52	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
54	53	an32s 846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
55	54	anassrs 680	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
56		oveq2 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
57	56	eleq1d 2686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
58	55, 57	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑠 ∈ 𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
59	58	rexlimdva 3031	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
60	59	adantld 483	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ((𝑣 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
61	33, 60	syl5bi 232	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
62	61	ralrimiv 2965	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
63	4, 9, 5	rngoass 33705	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
64	63	3exp2 1285	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → (𝑤 ∈ 𝑋 → (𝑟 ∈ 𝑋 → (𝐴 ∈ 𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
65	64	imp42 620	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
66	65	an32s 846	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
67	4, 9, 5	rngocl 33700	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
68	67	3expib 1268	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑅 ∈ RingOps → ((𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
69	68	imdistani 726	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
70	4, 9, 5	rngocl 33700	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
71	70	3expa 1265	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
72		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
73		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
74	73	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑤𝐻𝑟) → (((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)))
75	74	rspcev 3309	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
76	72, 75	mpan2 707	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
77	76	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
78		eqeq1 2626	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
79	78	rexbidv 3052	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
80	79	elrab 3363	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
81	71, 77, 80	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
82	69, 81	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) ∧ 𝐴 ∈ 𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
83	82	an32s 846	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
84	66, 83	eqeltrrd 2702	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ (𝑤 ∈ 𝑋 ∧ 𝑟 ∈ 𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
85	84	anass1rs 849	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
86	85	ralrimiva 2966	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
87	62, 86	jca 554	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
88		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
89	88	eleq1d 2686	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
90	89	ralbidv 2986	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
91		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
92	91	eleq1d 2686	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
93	92	ralbidv 2986	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑟𝐻𝐴) → (∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
94	90, 93	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
95	87, 94	syl5ibrcom 237	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ 𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
96	95	rexlimdva 3031	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
97	96	adantld 483	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((𝑢 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
98	26, 97	syl5bi 232	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
99	98	ralrimiv 2965	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))
100	3, 19, 99	3jca 1242	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
101	1, 100	sylan 488	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})))
102	4, 9, 5, 6	isidlc 33814	. . . . 5 ⊢ (𝑅 ∈ CRingOps → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))))
103	102	adantr 481	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤 ∈ 𝑋 (𝑤𝐻𝑢) ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}))))
104	101, 103	mpbird 247	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
105		simpr 477	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
106	4	rneqi 5352	. . . . . . . . . 10 ⊢ ran 𝐺 = ran (1^st ‘𝑅)
107	5, 106	eqtri 2644	. . . . . . . . 9 ⊢ 𝑋 = ran (1^st ‘𝑅)
108		eqid 2622	. . . . . . . . 9 ⊢ (GId‘𝐻) = (GId‘𝐻)
109	107, 9, 108	rngo1cl 33738	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
110	109	adantr 481	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → (GId‘𝐻) ∈ 𝑋)
111	9, 107, 108	rngolidm 33736	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
112	111	eqcomd 2628	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
113		oveq1 6657	. . . . . . . . 9 ⊢ (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
114	113	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑦 = (GId‘𝐻) → (𝐴 = (𝑦𝐻𝐴) ↔ 𝐴 = ((GId‘𝐻)𝐻𝐴)))
115	114	rspcev 3309	. . . . . . 7 ⊢ (((GId‘𝐻) ∈ 𝑋 ∧ 𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
116	110, 112, 115	syl2anc 693	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
117	1, 116	sylan 488	. . . . 5 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴))
118		eqeq1 2626	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
119	118	rexbidv 3052	. . . . . 6 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
120	119	elrab 3363	. . . . 5 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝐴 = (𝑦𝐻𝐴)))
121	105, 117, 120	sylanbrc 698	. . . 4 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
122	121	snssd 4340	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
123		snssg 4327	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ 𝑗 ↔ {𝐴} ⊆ 𝑗))
124	123	biimpar 502	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴 ∈ 𝑗)
125	4, 9, 5	idllmulcl 33819	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝑗 ∧ 𝑦 ∈ 𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
126	125	anassrs 680	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
127		eleq1 2689	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦𝐻𝐴) → (𝑥 ∈ 𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
128	126, 127	syl5ibrcom 237	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑦 ∈ 𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
129	128	rexlimdva 3031	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
130	129	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
131	130	ralrimiva 2966	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
132		rabss 3679	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥 ∈ 𝑋 (∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥 ∈ 𝑗))
133	131, 132	sylibr 224	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑗) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
134	133	ex 450	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴 ∈ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
135	124, 134	syl5 34	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴 ∈ 𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136	135	expdimp 453	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
137	136	an32s 846	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
138	137	ralrimiva 2966	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
139	1, 138	sylan 488	. . 3 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
140	104, 122, 139	3jca 1242	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
141		snssi 4339	. . 3 ⊢ (𝐴 ∈ 𝑋 → {𝐴} ⊆ 𝑋)
142	4, 5	igenval2 33865	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
143	1, 141, 142	syl2an 494	. 2 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
144	140, 143	mpbird 247	1 ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 {crab 2916 ⊆ wss 3574 {csn 4177 ran crn 5115 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 GIdcgi 27344 RingOpscrngo 33693 CRingOpsccring 33792 Idlcidl 33806 IdlGen cigen 33858

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-grpo 27347 df-gid 27348 df-ginv 27349 df-ablo 27399 df-ass 33642 df-exid 33644 df-mgmOLD 33648 df-sgrOLD 33660 df-mndo 33666 df-rngo 33694 df-com2 33789 df-crngo 33793 df-idl 33809 df-igen 33859

This theorem is referenced by: isfldidl 33867 ispridlc 33869

W3C validator