Theorem prnc 16215

Description: A principal ideal (an ideal generated by one element) in a commutative ring.

Hypotheses

Ref	Expression
prnc.1	|- G = (1st` R)
prnc.2	|- H = (2nd` R)
prnc.3	|- X = ran G

Assertion

Ref	Expression
prnc	|- ((R e. CRing /\ A e. X) -> (R IdlGen {A}) = {x e. X | E.y e. X x = (yHA)})

Distinct variable groups:   x,R,y   x,X,y   x,G,y   x,H,y   x,A,y

Proof of Theorem prnc

Step	Hyp	Ref	Expression
1		ssrab2 2692	. . . . . . 7 |- {x e. X | E.y e. X x = (yHA)} C_ X
2	1	a1i 8	. . . . . 6 |- ((R e. Ring /\ A e. X) -> {x e. X | E.y e. X x = (yHA)} C_ X)
3		eqeq1 1890	. . . . . . . . 9 |- (x = (Id` G) -> (x = (yHA) <-> (Id` G) = (yHA)))
4	3	rexbidv 2124	. . . . . . . 8 |- (x = (Id` G) -> (E.y e. X x = (yHA) <-> E.y e. X (Id` G) = (yHA)))
5	4	elrab 2414	. . . . . . 7 |- ((Id` G) e. {x e. X | E.y e. X x = (yHA)} <-> ((Id` G) e. X /\ E.y e. X (Id` G) = (yHA)))
6		prnc.1	. . . . . . . . 9 |- G = (1st` R)
7		prnc.3	. . . . . . . . 9 |- X = ran G
8		eqid 1884	. . . . . . . . 9 |- (Id` G) = (Id` G)
9	6, 7, 8	ring0cl 9484	. . . . . . . 8 |- (R e. Ring -> (Id` G) e. X)
10	9	adantr 425	. . . . . . 7 |- ((R e. Ring /\ A e. X) -> (Id` G) e. X)
11		prnc.2	. . . . . . . . . 10 |- H = (2nd` R)
12	8, 7, 6, 11	ringlz 9487	. . . . . . . . 9 |- ((R e. Ring /\ A e. X) -> ((Id` G)HA) = (Id` G))
13	12	eqcomd 1889	. . . . . . . 8 |- ((R e. Ring /\ A e. X) -> (Id` G) = ((Id` G)HA))
14		opreq1 4889	. . . . . . . . . 10 |- (y = (Id` G) -> (yHA) = ((Id` G)HA))
15	14	eqeq2d 1895	. . . . . . . . 9 |- (y = (Id` G) -> ((Id` G) = (yHA) <-> (Id` G) = ((Id` G)HA)))
16	15	rcla4ev 2381	. . . . . . . 8 |- (((Id` G) e. X /\ (Id` G) = ((Id` G)HA)) -> E.y e. X (Id` G) = (yHA))
17	10, 13, 16	syl11anc 524	. . . . . . 7 |- ((R e. Ring /\ A e. X) -> E.y e. X (Id` G) = (yHA))
18	5, 10, 17	sylanbrc 527	. . . . . 6 |- ((R e. Ring /\ A e. X) -> (Id` G) e. {x e. X | E.y e. X x = (yHA)})
19		opreq1 4889	. . . . . . . . . . . . . 14 |- (u = (rHA) -> (uGv) = ((rHA)Gv))
20	19	eleq1d 1963	. . . . . . . . . . . . 13 |- (u = (rHA) -> ((uGv) e. {x e. X | E.y e. X x = (yHA)} <-> ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)}))
21	20	ralbidv 2123	. . . . . . . . . . . 12 |- (u = (rHA) -> (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} <-> A.v e. {x e. X | E.y e. X x = (yHA)} ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)}))
22		opreq2 4890	. . . . . . . . . . . . . 14 |- (u = (rHA) -> (wHu) = (wH(rHA)))
23	22	eleq1d 1963	. . . . . . . . . . . . 13 |- (u = (rHA) -> ((wHu) e. {x e. X | E.y e. X x = (yHA)} <-> (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)}))
24	23	ralbidv 2123	. . . . . . . . . . . 12 |- (u = (rHA) -> (A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)} <-> A.w e. X (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)}))
25	21, 24	anbi12d 690	. . . . . . . . . . 11 |- (u = (rHA) -> ((A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)}) <-> (A.v e. {x e. X | E.y e. X x = (yHA)} ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)})))
26		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (v = (sHA) -> ((rHA)Gv) = ((rHA)G(sHA)))
27	26	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (v = (sHA) -> (((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)} <-> ((rHA)G(sHA)) e. {x e. X | E.y e. X x = (yHA)}))
28	6, 11, 7	ringdir 9472	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R e. Ring /\ (r e. X /\ s e. X /\ A e. X)) -> ((rGs)HA) = ((rHA)G(sHA)))
29	28	3exp2 1086	. . . . . . . . . . . . . . . . . . . . 21 |- (R e. Ring -> (r e. X -> (s e. X -> (A e. X -> ((rGs)HA) = ((rHA)G(sHA))))))
30	29	imp42 396	. . . . . . . . . . . . . . . . . . . 20 |- (((R e. Ring /\ (r e. X /\ s e. X)) /\ A e. X) -> ((rGs)HA) = ((rHA)G(sHA)))
31		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = ((rGs)HA) -> (x = (yHA) <-> ((rGs)HA) = (yHA)))
32	31	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = ((rGs)HA) -> (E.y e. X x = (yHA) <-> E.y e. X ((rGs)HA) = (yHA)))
33	32	elrab 2414	. . . . . . . . . . . . . . . . . . . . . 22 |- (((rGs)HA) e. {x e. X | E.y e. X x = (yHA)} <-> (((rGs)HA) e. X /\ E.y e. X ((rGs)HA) = (yHA)))
34	6, 11, 7	ringcl 9468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. Ring /\ (rGs) e. X /\ A e. X) -> ((rGs)HA) e. X)
35	34	3expa 1067	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. Ring /\ (rGs) e. X) /\ A e. X) -> ((rGs)HA) e. X)
36		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((rGs)HA) = ((rGs)HA)
37		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = (rGs) -> (yHA) = ((rGs)HA))
38	37	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = (rGs) -> (((rGs)HA) = (yHA) <-> ((rGs)HA) = ((rGs)HA)))
39	38	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((rGs) e. X /\ ((rGs)HA) = ((rGs)HA)) -> E.y e. X ((rGs)HA) = (yHA))
40	36, 39	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((rGs) e. X -> E.y e. X ((rGs)HA) = (yHA))
41	40	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. Ring /\ (rGs) e. X) /\ A e. X) -> E.y e. X ((rGs)HA) = (yHA))
42	33, 35, 41	sylanbrc 527	. . . . . . . . . . . . . . . . . . . . 21 |- (((R e. Ring /\ (rGs) e. X) /\ A e. X) -> ((rGs)HA) e. {x e. X | E.y e. X x = (yHA)})
43	6, 7	ringgcl 9477	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. Ring /\ r e. X /\ s e. X) -> (rGs) e. X)
44	43	3expib 1070	. . . . . . . . . . . . . . . . . . . . . 22 |- (R e. Ring -> ((r e. X /\ s e. X) -> (rGs) e. X))
45	44	imdistani 491	. . . . . . . . . . . . . . . . . . . . 21 |- ((R e. Ring /\ (r e. X /\ s e. X)) -> (R e. Ring /\ (rGs) e. X))
46	42, 45	sylan 497	. . . . . . . . . . . . . . . . . . . 20 |- (((R e. Ring /\ (r e. X /\ s e. X)) /\ A e. X) -> ((rGs)HA) e. {x e. X | E.y e. X x = (yHA)})
47	30, 46	eqeltrrd 1972	. . . . . . . . . . . . . . . . . . 19 |- (((R e. Ring /\ (r e. X /\ s e. X)) /\ A e. X) -> ((rHA)G(sHA)) e. {x e. X | E.y e. X x = (yHA)})
48	47	an1rs 547	. . . . . . . . . . . . . . . . . 18 |- (((R e. Ring /\ A e. X) /\ (r e. X /\ s e. X)) -> ((rHA)G(sHA)) e. {x e. X | E.y e. X x = (yHA)})
49	48	anassrs 489	. . . . . . . . . . . . . . . . 17 |- ((((R e. Ring /\ A e. X) /\ r e. X) /\ s e. X) -> ((rHA)G(sHA)) e. {x e. X | E.y e. X x = (yHA)})
50	27, 49	syl5cbir 228	. . . . . . . . . . . . . . . 16 |- ((((R e. Ring /\ A e. X) /\ r e. X) /\ s e. X) -> (v = (sHA) -> ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)}))
51	50	r19.23adva 2216	. . . . . . . . . . . . . . 15 |- (((R e. Ring /\ A e. X) /\ r e. X) -> (E.s e. X v = (sHA) -> ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)}))
52	51	adantld 426	. . . . . . . . . . . . . 14 |- (((R e. Ring /\ A e. X) /\ r e. X) -> ((v e. X /\ E.s e. X v = (sHA)) -> ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)}))
53		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (x = v -> (x = (yHA) <-> v = (yHA)))
54	53	rexbidv 2124	. . . . . . . . . . . . . . . 16 |- (x = v -> (E.y e. X x = (yHA) <-> E.y e. X v = (yHA)))
55		opreq1 4889	. . . . . . . . . . . . . . . . . 18 |- (y = s -> (yHA) = (sHA))
56	55	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (y = s -> (v = (yHA) <-> v = (sHA)))
57	56	cbvrexv 2281	. . . . . . . . . . . . . . . 16 |- (E.y e. X v = (yHA) <-> E.s e. X v = (sHA))
58	54, 57	syl6bb 595	. . . . . . . . . . . . . . 15 |- (x = v -> (E.y e. X x = (yHA) <-> E.s e. X v = (sHA)))
59	58	elrab 2414	. . . . . . . . . . . . . 14 |- (v e. {x e. X | E.y e. X x = (yHA)} <-> (v e. X /\ E.s e. X v = (sHA)))
60	52, 59	syl5ib 223	. . . . . . . . . . . . 13 |- (((R e. Ring /\ A e. X) /\ r e. X) -> (v e. {x e. X | E.y e. X x = (yHA)} -> ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)}))
61	60	r19.21aiv 2175	. . . . . . . . . . . 12 |- (((R e. Ring /\ A e. X) /\ r e. X) -> A.v e. {x e. X | E.y e. X x = (yHA)} ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)})
62	6, 11, 7	ringass 9473	. . . . . . . . . . . . . . . . . 18 |- ((R e. Ring /\ (w e. X /\ r e. X /\ A e. X)) -> ((wHr)HA) = (wH(rHA)))
63	62	3exp2 1086	. . . . . . . . . . . . . . . . 17 |- (R e. Ring -> (w e. X -> (r e. X -> (A e. X -> ((wHr)HA) = (wH(rHA))))))
64	63	imp42 396	. . . . . . . . . . . . . . . 16 |- (((R e. Ring /\ (w e. X /\ r e. X)) /\ A e. X) -> ((wHr)HA) = (wH(rHA)))
65	64	an1rs 547	. . . . . . . . . . . . . . 15 |- (((R e. Ring /\ A e. X) /\ (w e. X /\ r e. X)) -> ((wHr)HA) = (wH(rHA)))
66		eqeq1 1890	. . . . . . . . . . . . . . . . . . . 20 |- (x = ((wHr)HA) -> (x = (yHA) <-> ((wHr)HA) = (yHA)))
67	66	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (x = ((wHr)HA) -> (E.y e. X x = (yHA) <-> E.y e. X ((wHr)HA) = (yHA)))
68	67	elrab 2414	. . . . . . . . . . . . . . . . . 18 |- (((wHr)HA) e. {x e. X | E.y e. X x = (yHA)} <-> (((wHr)HA) e. X /\ E.y e. X ((wHr)HA) = (yHA)))
69	6, 11, 7	ringcl 9468	. . . . . . . . . . . . . . . . . . 19 |- ((R e. Ring /\ (wHr) e. X /\ A e. X) -> ((wHr)HA) e. X)
70	69	3expa 1067	. . . . . . . . . . . . . . . . . 18 |- (((R e. Ring /\ (wHr) e. X) /\ A e. X) -> ((wHr)HA) e. X)
71		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- ((wHr)HA) = ((wHr)HA)
72		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (wHr) -> (yHA) = ((wHr)HA))
73	72	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (wHr) -> (((wHr)HA) = (yHA) <-> ((wHr)HA) = ((wHr)HA)))
74	73	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- (((wHr) e. X /\ ((wHr)HA) = ((wHr)HA)) -> E.y e. X ((wHr)HA) = (yHA))
75	71, 74	mpan2 760	. . . . . . . . . . . . . . . . . . 19 |- ((wHr) e. X -> E.y e. X ((wHr)HA) = (yHA))
76	75	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- (((R e. Ring /\ (wHr) e. X) /\ A e. X) -> E.y e. X ((wHr)HA) = (yHA))
77	68, 70, 76	sylanbrc 527	. . . . . . . . . . . . . . . . 17 |- (((R e. Ring /\ (wHr) e. X) /\ A e. X) -> ((wHr)HA) e. {x e. X | E.y e. X x = (yHA)})
78	6, 11, 7	ringcl 9468	. . . . . . . . . . . . . . . . . . 19 |- ((R e. Ring /\ w e. X /\ r e. X) -> (wHr) e. X)
79	78	3expib 1070	. . . . . . . . . . . . . . . . . 18 |- (R e. Ring -> ((w e. X /\ r e. X) -> (wHr) e. X))
80	79	imdistani 491	. . . . . . . . . . . . . . . . 17 |- ((R e. Ring /\ (w e. X /\ r e. X)) -> (R e. Ring /\ (wHr) e. X))
81	77, 80	sylan 497	. . . . . . . . . . . . . . . 16 |- (((R e. Ring /\ (w e. X /\ r e. X)) /\ A e. X) -> ((wHr)HA) e. {x e. X | E.y e. X x = (yHA)})
82	81	an1rs 547	. . . . . . . . . . . . . . 15 |- (((R e. Ring /\ A e. X) /\ (w e. X /\ r e. X)) -> ((wHr)HA) e. {x e. X | E.y e. X x = (yHA)})
83	65, 82	eqeltrrd 1972	. . . . . . . . . . . . . 14 |- (((R e. Ring /\ A e. X) /\ (w e. X /\ r e. X)) -> (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)})
84	83	anass1rs 15646	. . . . . . . . . . . . 13 |- ((((R e. Ring /\ A e. X) /\ r e. X) /\ w e. X) -> (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)})
85	84	r19.21aiva 2176	. . . . . . . . . . . 12 |- (((R e. Ring /\ A e. X) /\ r e. X) -> A.w e. X (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)})
86	61, 85	jca 310	. . . . . . . . . . 11 |- (((R e. Ring /\ A e. X) /\ r e. X) -> (A.v e. {x e. X | E.y e. X x = (yHA)} ((rHA)Gv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wH(rHA)) e. {x e. X | E.y e. X x = (yHA)}))
87	25, 86	syl5cbir 228	. . . . . . . . . 10 |- (((R e. Ring /\ A e. X) /\ r e. X) -> (u = (rHA) -> (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)})))
88	87	r19.23adva 2216	. . . . . . . . 9 |- ((R e. Ring /\ A e. X) -> (E.r e. X u = (rHA) -> (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)})))
89	88	adantld 426	. . . . . . . 8 |- ((R e. Ring /\ A e. X) -> ((u e. X /\ E.r e. X u = (rHA)) -> (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)})))
90		eqeq1 1890	. . . . . . . . . . 11 |- (x = u -> (x = (yHA) <-> u = (yHA)))
91	90	rexbidv 2124	. . . . . . . . . 10 |- (x = u -> (E.y e. X x = (yHA) <-> E.y e. X u = (yHA)))
92		opreq1 4889	. . . . . . . . . . . 12 |- (y = r -> (yHA) = (rHA))
93	92	eqeq2d 1895	. . . . . . . . . . 11 |- (y = r -> (u = (yHA) <-> u = (rHA)))
94	93	cbvrexv 2281	. . . . . . . . . 10 |- (E.y e. X u = (yHA) <-> E.r e. X u = (rHA))
95	91, 94	syl6bb 595	. . . . . . . . 9 |- (x = u -> (E.y e. X x = (yHA) <-> E.r e. X u = (rHA)))
96	95	elrab 2414	. . . . . . . 8 |- (u e. {x e. X | E.y e. X x = (yHA)} <-> (u e. X /\ E.r e. X u = (rHA)))
97	89, 96	syl5ib 223	. . . . . . 7 |- ((R e. Ring /\ A e. X) -> (u e. {x e. X | E.y e. X x = (yHA)} -> (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)})))
98	97	r19.21aiv 2175	. . . . . 6 |- ((R e. Ring /\ A e. X) -> A.u e. {x e. X | E.y e. X x = (yHA)} (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)}))
99	2, 18, 98	3jca 1050	. . . . 5 |- ((R e. Ring /\ A e. X) -> ({x e. X | E.y e. X x = (yHA)} C_ X /\ (Id` G) e. {x e. X | E.y e. X x = (yHA)} /\ A.u e. {x e. X | E.y e. X x = (yHA)} (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)})))
100		crngrng 16148	. . . . 5 |- (R e. CRing -> R e. Ring)
101	99, 100	sylan 497	. . . 4 |- ((R e. CRing /\ A e. X) -> ({x e. X | E.y e. X x = (yHA)} C_ X /\ (Id` G) e. {x e. X | E.y e. X x = (yHA)} /\ A.u e. {x e. X | E.y e. X x = (yHA)} (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)})))
102	6, 11, 7, 8	isidlc 16163	. . . . 5 |- (R e. CRing -> ({x e. X | E.y e. X x = (yHA)} e. (Idl` R) <-> ({x e. X | E.y e. X x = (yHA)} C_ X /\ (Id` G) e. {x e. X | E.y e. X x = (yHA)} /\ A.u e. {x e. X | E.y e. X x = (yHA)} (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)}))))
103	102	adantr 425	. . . 4 |- ((R e. CRing /\ A e. X) -> ({x e. X | E.y e. X x = (yHA)} e. (Idl` R) <-> ({x e. X | E.y e. X x = (yHA)} C_ X /\ (Id` G) e. {x e. X | E.y e. X x = (yHA)} /\ A.u e. {x e. X | E.y e. X x = (yHA)} (A.v e. {x e. X | E.y e. X x = (yHA)} (uGv) e. {x e. X | E.y e. X x = (yHA)} /\ A.w e. X (wHu) e. {x e. X | E.y e. X x = (yHA)}))))
104	101, 103	mpbird 213	. . 3 |- ((R e. CRing /\ A e. X) -> {x e. X | E.y e. X x = (yHA)} e. (Idl` R))
105		eqeq1 1890	. . . . . . 7 |- (x = A -> (x = (yHA) <-> A = (yHA)))
106	105	rexbidv 2124	. . . . . 6 |- (x = A -> (E.y e. X x = (yHA) <-> E.y e. X A = (yHA)))
107	106	elrab 2414	. . . . 5 |- (A e. {x e. X | E.y e. X x = (yHA)} <-> (A e. X /\ E.y e. X A = (yHA)))
108		simpr 350	. . . . 5 |- ((R e. CRing /\ A e. X) -> A e. X)
109	6	rneqi 4187	. . . . . . . . . 10 |- ran G = ran (1st` R)
110	7, 109	eqtri 1908	. . . . . . . . 9 |- X = ran (1st` R)
111		eqid 1884	. . . . . . . . 9 |- (Id` H) = (Id` H)
112	110, 11, 111	ring1cl 10415	. . . . . . . 8 |- (R e. Ring -> (Id` H) e. X)
113	112	adantr 425	. . . . . . 7 |- ((R e. Ring /\ A e. X) -> (Id` H) e. X)
114	11, 110, 111	ringlidm 10410	. . . . . . . 8 |- ((R e. Ring /\ A e. X) -> ((Id` H)HA) = A)
115	114	eqcomd 1889	. . . . . . 7 |- ((R e. Ring /\ A e. X) -> A = ((Id` H)HA))
116		opreq1 4889	. . . . . . . . 9 |- (y = (Id` H) -> (yHA) = ((Id` H)HA))
117	116	eqeq2d 1895	. . . . . . . 8 |- (y = (Id` H) -> (A = (yHA) <-> A = ((Id` H)HA)))
118	117	rcla4ev 2381	. . . . . . 7 |- (((Id` H) e. X /\ A = ((Id` H)HA)) -> E.y e. X A = (yHA))
119	113, 115, 118	syl11anc 524	. . . . . 6 |- ((R e. Ring /\ A e. X) -> E.y e. X A = (yHA))
120	119, 100	sylan 497	. . . . 5 |- ((R e. CRing /\ A e. X) -> E.y e. X A = (yHA))
121	107, 108, 120	sylanbrc 527	. . . 4 |- ((R e. CRing /\ A e. X) -> A e. {x e. X | E.y e. X x = (yHA)})
122	121	snssd 3130	. . 3 |- ((R e. CRing /\ A e. X) -> {A} C_ {x e. X | E.y e. X x = (yHA)})
123		eleq1 1957	. . . . . . . . . . . . . 14 |- (x = (yHA) -> (x e. j <-> (yHA) e. j))
124	6, 11, 7	idllmulcl 16168	. . . . . . . . . . . . . . 15 |- (((R e. Ring /\ j e. (Idl` R)) /\ (A e. j /\ y e. X)) -> (yHA) e. j)
125	124	anassrs 489	. . . . . . . . . . . . . 14 |- ((((R e. Ring /\ j e. (Idl` R)) /\ A e. j) /\ y e. X) -> (yHA) e. j)
126	123, 125	syl5cbir 228	. . . . . . . . . . . . 13 |- ((((R e. Ring /\ j e. (Idl` R)) /\ A e. j) /\ y e. X) -> (x = (yHA) -> x e. j))
127	126	r19.23adva 2216	. . . . . . . . . . . 12 |- (((R e. Ring /\ j e. (Idl` R)) /\ A e. j) -> (E.y e. X x = (yHA) -> x e. j))
128	127	adantr 425	. . . . . . . . . . 11 |- ((((R e. Ring /\ j e. (Idl` R)) /\ A e. j) /\ x e. X) -> (E.y e. X x = (yHA) -> x e. j))
129	128	r19.21aiva 2176	. . . . . . . . . 10 |- (((R e. Ring /\ j e. (Idl` R)) /\ A e. j) -> A.x e. X (E.y e. X x = (yHA) -> x e. j))
130		rabss 2684	. . . . . . . . . 10 |- ({x e. X | E.y e. X x = (yHA)} C_ j <-> A.x e. X (E.y e. X x = (yHA) -> x e. j))
131	129, 130	sylibr 217	. . . . . . . . 9 |- (((R e. Ring /\ j e. (Idl` R)) /\ A e. j) -> {x e. X | E.y e. X x = (yHA)} C_ j)
132	131	ex 402	. . . . . . . 8 |- ((R e. Ring /\ j e. (Idl` R)) -> (A e. j -> {x e. X | E.y e. X x = (yHA)} C_ j))
133		snssg 3124	. . . . . . . . 9 |- (A e. X -> (A e. j <-> {A} C_ j))
134	133	biimpar 461	. . . . . . . 8 |- ((A e. X /\ {A} C_ j) -> A e. j)
135	132, 134	syl5 20	. . . . . . 7 |- ((R e. Ring /\ j e. (Idl` R)) -> ((A e. X /\ {A} C_ j) -> {x e. X | E.y e. X x = (yHA)} C_ j))
136	135	expdimp 406	. . . . . 6 |- (((R e. Ring /\ j e. (Idl` R)) /\ A e. X) -> ({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j))
137	136	an1rs 547	. . . . 5 |- (((R e. Ring /\ A e. X) /\ j e. (Idl` R)) -> ({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j))
138	137	r19.21aiva 2176	. . . 4 |- ((R e. Ring /\ A e. X) -> A.j e. (Idl` R)({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j))
139	138, 100	sylan 497	. . 3 |- ((R e. CRing /\ A e. X) -> A.j e. (Idl` R)({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j))
140	104, 122, 139	3jca 1050	. 2 |- ((R e. CRing /\ A e. X) -> ({x e. X | E.y e. X x = (yHA)} e. (Idl` R) /\ {A} C_ {x e. X | E.y e. X x = (yHA)} /\ A.j e. (Idl` R)({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j)))
141	6, 7	igenval2 16214	. . 3 |- ((R e. Ring /\ {A} C_ X) -> ((R IdlGen {A}) = {x e. X | E.y e. X x = (yHA)} <-> ({x e. X | E.y e. X x = (yHA)} e. (Idl` R) /\ {A} C_ {x e. X | E.y e. X x = (yHA)} /\ A.j e. (Idl` R)({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j))))
142		snssi 3129	. . 3 |- (A e. X -> {A} C_ X)
143	141, 100, 142	syl2an 503	. 2 |- ((R e. CRing /\ A e. X) -> ((R IdlGen {A}) = {x e. X | E.y e. X x = (yHA)} <-> ({x e. X | E.y e. X x = (yHA)} e. (Idl` R) /\ {A} C_ {x e. X | E.y e. X x = (yHA)} /\ A.j e. (Idl` R)({A} C_ j -> {x e. X | E.y e. X x = (yHA)} C_ j))))
144	140, 143	mpbird 213	1 |- ((R e. CRing /\ A e. X) -> (R IdlGen {A}) = {x e. X | E.y e. X x = (yHA)})

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {crab 2108   C_ wss 2593  {csn 3044  ran crn 3987  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019  Idcgi 9312  Ringcring 9463  CRingccring 16143  Idlcidl 16155   IdlGen cigen 16207

This theorem is referenced by:  isfldidl 16216  ispridlc 16218

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-grp 9316  df-gid 9317  df-ginv 9318  df-abl 9408  df-ring 9464  df-ass 10360  df-exid 10362  df-mgm 10366  df-sgr 10378  df-mnd 10385  df-com2 10395  df-cring 16144  df-idl 16158  df-igen 16208

Copyright terms: Public domain