Metamath Proof Explorer

Theorem rngoidmlem

Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses uridm.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
uridm.2 ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
uridm.3 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion rngoidmlem ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 uridm.1 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2 uridm.2 ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
3 uridm.3 ⊢ 𝑈 = ( GId ‘ 𝐻 )
4 1 rngomndo ⊢ ( 𝑅 ∈ RingOps → 𝐻 ∈ MndOp )
5 mndomgmid ⊢ ( 𝐻 ∈ MndOp → 𝐻 ∈ ( Magma ∩ ExId ) )
6 eqid ⊢ ran 𝐻 = ran 𝐻
7 6 3 cmpidelt ⊢ ( ( 𝐻 ∈ ( Magma ∩ ExId ) ∧ 𝐴 ∈ ran 𝐻 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )
8 7 ex ⊢ ( 𝐻 ∈ ( Magma ∩ ExId ) → ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) )
9 4 5 8 3syl ⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) )
10 eqid ⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
11 1 10 rngorn1eq ⊢ ( 𝑅 ∈ RingOps → ran ( 1st ‘ 𝑅 ) = ran 𝐻 )
12 eqtr ⊢ ( ( 𝑋 = ran ( 1st ‘ 𝑅 ) ∧ ran ( 1st ‘ 𝑅 ) = ran 𝐻 ) → 𝑋 = ran 𝐻 )
13 simpl ⊢ ( ( 𝑋 = ran 𝐻 ∧ 𝑅 ∈ RingOps ) → 𝑋 = ran 𝐻 )
14 13 eleq2d ⊢ ( ( 𝑋 = ran 𝐻 ∧ 𝑅 ∈ RingOps ) → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ran 𝐻 ) )
15 14 imbi1d ⊢ ( ( 𝑋 = ran 𝐻 ∧ 𝑅 ∈ RingOps ) → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) )
16 15 ex ⊢ ( 𝑋 = ran 𝐻 → ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) ) )
17 12 16 syl ⊢ ( ( 𝑋 = ran ( 1st ‘ 𝑅 ) ∧ ran ( 1st ‘ 𝑅 ) = ran 𝐻 ) → ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) ) )
18 2 17 mpan ⊢ ( ran ( 1st ‘ 𝑅 ) = ran 𝐻 → ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) ) )
19 11 18 mpcom ⊢ ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) )
20 9 19 mpbird ⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) )
21 20 imp ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )