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 ⊢ H = 2 nd ⁡ R
uridm.2 ⊢ X = ran ⁡ 1 st ⁡ R
uridm.3 ⊢ U = GId ⁡ H
Assertion rngoidmlem ⊢ R ∈ RingOps ∧ A ∈ X → U H A = A ∧ A H U = A

Proof

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