This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐼 ∈ 𝑈 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐼 = ( 𝐾 ‘ { 𝐺 } ) ↔ ( 𝐺 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 𝐺 ∥ 𝑥 ) ) )