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

Metamath Proof Explorer

Theorem rngo2

Description: A ring element plus itself is two times the element. (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 rngo2 ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ringi.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ringi.3 ⊢ 𝑋 = ran 𝐺
4 1 2 3 rngoid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑥 ) = 𝐴 ) )
5 oveq12 ⊢ ( ( ( 𝑥 𝐻 𝐴 ) = 𝐴 ∧ ( 𝑥 𝐻 𝐴 ) = 𝐴 ) → ( ( 𝑥 𝐻 𝐴 ) 𝐺 ( 𝑥 𝐻 𝐴 ) ) = ( 𝐴 𝐺 𝐴 ) )
6 5 anidms ⊢ ( ( 𝑥 𝐻 𝐴 ) = 𝐴 → ( ( 𝑥 𝐻 𝐴 ) 𝐺 ( 𝑥 𝐻 𝐴 ) ) = ( 𝐴 𝐺 𝐴 ) )
7 6 eqcomd ⊢ ( ( 𝑥 𝐻 𝐴 ) = 𝐴 → ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐻 𝐴 ) 𝐺 ( 𝑥 𝐻 𝐴 ) ) )
8 simpll ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ RingOps )
9 simpr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
10 simplr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
11 1 2 3 rngodir ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) = ( ( 𝑥 𝐻 𝐴 ) 𝐺 ( 𝑥 𝐻 𝐴 ) ) )
12 8 9 9 10 11 syl13anc ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) = ( ( 𝑥 𝐻 𝐴 ) 𝐺 ( 𝑥 𝐻 𝐴 ) ) )
13 12 eqeq2d ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ↔ ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐻 𝐴 ) 𝐺 ( 𝑥 𝐻 𝐴 ) ) ) )
14 7 13 imbitrrid ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 𝐻 𝐴 ) = 𝐴 → ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ) )
15 14 adantrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑥 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑥 ) = 𝐴 ) → ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ) )
16 15 reximdva ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑥 ) = 𝐴 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ) )
17 4 16 mpd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) )