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	syl5ibr	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 𝐻 𝐴 ) = 𝐴 → ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ) )
15	14	adantrd	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑥 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑥 ) = 𝐴 ) → ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ) )
16	15	reximdva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ( ( 𝑥 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑥 ) = 𝐴 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) ) )
17	4 16	mpd	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝐺 𝐴 ) = ( ( 𝑥 𝐺 𝑥 ) 𝐻 𝐴 ) )