Metamath Proof Explorer

Theorem igenval2

Description: The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses igenval2.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
igenval2.2 ⊢ 𝑋 = ran 𝐺
Assertion igenval2 ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 ↔ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) )

Proof

Step Hyp Ref Expression
1 igenval2.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 igenval2.2 ⊢ 𝑋 = ran 𝐺
3 1 2 igenidl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) ∈ ( Idl ‘ 𝑅 ) )
4 1 2 igenss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( 𝑅 IdlGen 𝑆 ) )
5 igenmin ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝑗 ) → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 )
6 5 3expia ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) )
7 6 ralrimiva ⊢ ( 𝑅 ∈ RingOps → ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) )
8 7 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) )
9 3 4 8 3jca ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑅 IdlGen 𝑆 ) ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ ( 𝑅 IdlGen 𝑆 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) ) )
10 eleq1 ⊢ ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( ( 𝑅 IdlGen 𝑆 ) ∈ ( Idl ‘ 𝑅 ) ↔ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) )
11 sseq2 ⊢ ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( 𝑆 ⊆ ( 𝑅 IdlGen 𝑆 ) ↔ 𝑆 ⊆ 𝐼 ) )
12 sseq1 ⊢ ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ↔ 𝐼 ⊆ 𝑗 ) )
13 12 imbi2d ⊢ ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) ↔ ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) )
14 13 ralbidv ⊢ ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) ↔ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) )
15 10 11 14 3anbi123d ⊢ ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( ( ( 𝑅 IdlGen 𝑆 ) ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ ( 𝑅 IdlGen 𝑆 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝑗 ) ) ↔ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) )
16 9 15 syl5ibcom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) )
17 igenmin ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝐼 )
18 17 3adant3r3 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝐼 )
19 18 adantlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝐼 )
20 ssint ⊢ ( 𝐼 ⊆ ∩ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } ↔ ∀ 𝑗 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } 𝐼 ⊆ 𝑗 )
21 sseq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑆 ⊆ 𝑖 ↔ 𝑆 ⊆ 𝑗 ) )
22 21 ralrab ⊢ ( ∀ 𝑗 ∈ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } 𝐼 ⊆ 𝑗 ↔ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) )
23 20 22 sylbbr ⊢ ( ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) → 𝐼 ⊆ ∩ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } )
24 23 3ad2ant3 ⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) → 𝐼 ⊆ ∩ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } )
25 24 adantl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) → 𝐼 ⊆ ∩ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } )
26 1 2 igenval ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } )
27 26 adantr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑖 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑖 } )
28 25 27 sseqtrrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) → 𝐼 ⊆ ( 𝑅 IdlGen 𝑆 ) )
29 19 28 eqssd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) → ( 𝑅 IdlGen 𝑆 ) = 𝐼 )
30 29 ex ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) → ( 𝑅 IdlGen 𝑆 ) = 𝐼 ) )
31 16 30 impbid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑅 IdlGen 𝑆 ) = 𝐼 ↔ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( 𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗 ) ) ) )