Metamath Proof Explorer

Theorem 1idl

Description: Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses 1idl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
1idl.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
1idl.3 ⊢ 𝑋 = ran 𝐺
1idl.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion 1idl ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 1idl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 1idl.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 1idl.3 ⊢ 𝑋 = ran 𝐺
4 1idl.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
5 1 3 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ 𝑋 )
6 5 adantr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑈 ∈ 𝐼 ) → 𝐼 ⊆ 𝑋 )
7 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
8 3 7 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
9 2 8 4 rngolidm ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑥 ) = 𝑥 )
10 9 ad2ant2rl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑈 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑈 𝐻 𝑥 ) = 𝑥 )
11 1 2 3 idlrmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑈 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑈 𝐻 𝑥 ) ∈ 𝐼 )
12 10 11 eqeltrrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑈 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ 𝐼 )
13 12 expr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑈 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ 𝐼 ) )
14 13 ssrdv ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑈 ∈ 𝐼 ) → 𝑋 ⊆ 𝐼 )
15 6 14 eqssd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑈 ∈ 𝐼 ) → 𝐼 = 𝑋 )
16 15 ex ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑈 ∈ 𝐼 → 𝐼 = 𝑋 ) )
17 8 2 4 rngo1cl ⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )
18 17 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝑈 ∈ 𝑋 )
19 eleq2 ⊢ ( 𝐼 = 𝑋 → ( 𝑈 ∈ 𝐼 ↔ 𝑈 ∈ 𝑋 ) )
20 18 19 syl5ibrcom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 = 𝑋 → 𝑈 ∈ 𝐼 ) )
21 16 20 impbid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋 ) )