This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngoid

Description: The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringi.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ringi.3 ⊢ 𝑋 = ran 𝐺
Assertion rngoid ( ( 𝑅 ∈ 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 r19.12 ⊢ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
7 5 6 syl ⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
8 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑢 𝐻 𝑥 ) = ( 𝑢 𝐻 𝐴 ) )
9 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
10 8 9 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐻 𝐴 ) = 𝐴 ) )
11 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 𝑢 ) = ( 𝐴 𝐻 𝑢 ) )
12 11 9 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐻 𝑢 ) = 𝑥 ↔ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )
13 10 12 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) ) )
14 13 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) ) )
15 14 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )
16 7 15 sylan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑢 ) = 𝐴 ) )