Metamath Proof Explorer

Theorem rngoideu

Description: The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringi.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ringi.3 ⊢ 𝑋 = ran 𝐺
Assertion rngoideu ( 𝑅 ∈ RingOps → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ringi.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ringi.3 ⊢ 𝑋 = ran 𝐺
4 1 2 3 rngoi ⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑢 𝐻 𝑥 ) 𝐻 𝑦 ) = ( 𝑢 𝐻 ( 𝑥 𝐻 𝑦 ) ) ∧ ( 𝑢 𝐻 ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑢 𝐻 𝑥 ) 𝐺 ( 𝑢 𝐻 𝑦 ) ) ∧ ( ( 𝑢 𝐺 𝑥 ) 𝐻 𝑦 ) = ( ( 𝑢 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑦 ) ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) ) )
5 4 simprrd ⊢ ( 𝑅 ∈ RingOps → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
6 simpl ⊢ ( ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) → ( 𝑢 𝐻 𝑥 ) = 𝑥 )
7 6 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐻 𝑥 ) = 𝑥 )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑢 𝐻 𝑥 ) = ( 𝑢 𝐻 𝑦 ) )
9 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
10 8 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐻 𝑦 ) = 𝑦 ) )
11 10 rspcv ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐻 𝑥 ) = 𝑥 → ( 𝑢 𝐻 𝑦 ) = 𝑦 ) )
12 7 11 syl5 ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) → ( 𝑢 𝐻 𝑦 ) = 𝑦 ) )
13 simpr ⊢ ( ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) → ( 𝑥 𝐻 𝑦 ) = 𝑥 )
14 13 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = 𝑥 )
15 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 𝐻 𝑦 ) = ( 𝑢 𝐻 𝑦 ) )
16 id ⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 )
17 15 16 eqeq12d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 𝐻 𝑦 ) = 𝑥 ↔ ( 𝑢 𝐻 𝑦 ) = 𝑢 ) )
18 17 rspcv ⊢ ( 𝑢 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) = 𝑥 → ( 𝑢 𝐻 𝑦 ) = 𝑢 ) )
19 14 18 syl5 ⊢ ( 𝑢 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) → ( 𝑢 𝐻 𝑦 ) = 𝑢 ) )
20 12 19 im2anan9r ⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) ) → ( ( 𝑢 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑢 𝐻 𝑦 ) = 𝑢 ) ) )
21 eqtr2 ⊢ ( ( ( 𝑢 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑢 𝐻 𝑦 ) = 𝑢 ) → 𝑦 = 𝑢 )
22 21 equcomd ⊢ ( ( ( 𝑢 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑢 𝐻 𝑦 ) = 𝑢 ) → 𝑢 = 𝑦 )
23 20 22 syl6 ⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) ) → 𝑢 = 𝑦 ) )
24 23 rgen2 ⊢ ∀ 𝑢 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) ) → 𝑢 = 𝑦 )
25 oveq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 𝐻 𝑥 ) = ( 𝑦 𝐻 𝑥 ) )
26 25 eqeq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑦 𝐻 𝑥 ) = 𝑥 ) )
27 26 ovanraleqv ⊢ ( 𝑢 = 𝑦 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) ) )
28 27 reu4 ⊢ ( ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑦 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑦 ) = 𝑥 ) ) → 𝑢 = 𝑦 ) ) )
29 5 24 28 sylanblrc ⊢ ( 𝑅 ∈ RingOps → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )