Theorem lidldvgen

Description: An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidldvgen.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lidldvgen.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lidldvgen.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	lidldvgen.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion	lidldvgen	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) ↔ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lidldvgen.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		lidldvgen.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
3		lidldvgen.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4		lidldvgen.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
5		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ Ring )
6		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
7	6	snssd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → { 𝐺 } ⊆ 𝐵 )
8	3 1	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝐺 } ⊆ 𝐵 ) → { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) )
9	5 7 8	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) )
10		snssg	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) ) )
11	10	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) ) )
12	9 11	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) )
13	1 3 4	rspsn	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑦 ∣ 𝐺 ∥ 𝑦 } )
14	13	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑦 ∣ 𝐺 ∥ 𝑦 } )
15	14	eleq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ 𝑥 ∈ { 𝑦 ∣ 𝐺 ∥ 𝑦 } ) )
16		vex	⊢ 𝑥 ∈ V
17		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝐺 ∥ 𝑦 ↔ 𝐺 ∥ 𝑥 ) )
18	16 17	elab	⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝐺 ∥ 𝑦 } ↔ 𝐺 ∥ 𝑥 )
19	15 18	bitrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ 𝐺 ∥ 𝑥 ) )
20	19	biimpd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) → 𝐺 ∥ 𝑥 ) )
21	20	ralrimiv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) 𝐺 ∥ 𝑥 )
22	12 21	jca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ∧ ∀ 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) 𝐺 ∥ 𝑥 ) )
23		eleq2	⊢ ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) → ( 𝐺 ∈ 𝐼 ↔ 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ) )
24		raleq	⊢ ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) → ( ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ↔ ∀ 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) 𝐺 ∥ 𝑥 ) )
25	23 24	anbi12d	⊢ ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) → ( ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ↔ ( 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ∧ ∀ 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) 𝐺 ∥ 𝑥 ) ) )
26	22 25	syl5ibrcom	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) → ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) )
27		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐼 → 𝐺 ∥ 𝑥 ) )
28		ssab	⊢ ( 𝐼 ⊆ { 𝑥 ∣ 𝐺 ∥ 𝑥 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐼 → 𝐺 ∥ 𝑥 ) )
29	27 28	sylbb2	⊢ ( ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 → 𝐼 ⊆ { 𝑥 ∣ 𝐺 ∥ 𝑥 } )
30	29	ad2antll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) → 𝐼 ⊆ { 𝑥 ∣ 𝐺 ∥ 𝑥 } )
31	1 3 4	rspsn	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑥 ∣ 𝐺 ∥ 𝑥 } )
32	31	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑥 ∣ 𝐺 ∥ 𝑥 } )
33	32	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑥 ∣ 𝐺 ∥ 𝑥 } )
34	30 33	sseqtrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) → 𝐼 ⊆ ( 𝐾 ‘ { 𝐺 } ) )
35		simpl1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐺 ∈ 𝐼 ) → 𝑅 ∈ Ring )
36		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐺 ∈ 𝐼 ) → 𝐼 ∈ 𝑈 )
37		snssi	⊢ ( 𝐺 ∈ 𝐼 → { 𝐺 } ⊆ 𝐼 )
38	37	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐺 ∈ 𝐼 ) → { 𝐺 } ⊆ 𝐼 )
39	3 2	rspssp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ { 𝐺 } ⊆ 𝐼 ) → ( 𝐾 ‘ { 𝐺 } ) ⊆ 𝐼 )
40	35 36 38 39	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐺 ∈ 𝐼 ) → ( 𝐾 ‘ { 𝐺 } ) ⊆ 𝐼 )
41	40	adantrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) → ( 𝐾 ‘ { 𝐺 } ) ⊆ 𝐼 )
42	34 41	eqssd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) → 𝐼 = ( 𝐾 ‘ { 𝐺 } ) )
43	42	ex	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) → 𝐼 = ( 𝐾 ‘ { 𝐺 } ) ) )
44	26 43	impbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) ↔ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) )