Theorem ringadd2

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) (Revised by AV, 24-Aug-2021)

	Ref	Expression
Hypotheses	ringadd2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringadd2.p	⊢ + = ( +g ‘ 𝑅 )
	ringadd2.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	ringadd2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 + 𝑋 ) = ( ( 𝑥 + 𝑥 ) · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ringadd2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringadd2.p	⊢ + = ( +g ‘ 𝑅 )
3		ringadd2.t	⊢ · = ( .r ‘ 𝑅 )
4	1 3	ringid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ( ( 𝑥 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑥 ) = 𝑋 ) )
5		oveq12	⊢ ( ( ( 𝑥 · 𝑋 ) = 𝑋 ∧ ( 𝑥 · 𝑋 ) = 𝑋 ) → ( ( 𝑥 · 𝑋 ) + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + 𝑋 ) )
6	5	anidms	⊢ ( ( 𝑥 · 𝑋 ) = 𝑋 → ( ( 𝑥 · 𝑋 ) + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + 𝑋 ) )
7	6	eqcomd	⊢ ( ( 𝑥 · 𝑋 ) = 𝑋 → ( 𝑋 + 𝑋 ) = ( ( 𝑥 · 𝑋 ) + ( 𝑥 · 𝑋 ) ) )
8		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
9		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
10		simplr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11	1 2 3	ringdir	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑥 ) · 𝑋 ) = ( ( 𝑥 · 𝑋 ) + ( 𝑥 · 𝑋 ) ) )
12	8 9 9 10 11	syl13anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 + 𝑥 ) · 𝑋 ) = ( ( 𝑥 · 𝑋 ) + ( 𝑥 · 𝑋 ) ) )
13	12	eqeq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑋 + 𝑋 ) = ( ( 𝑥 + 𝑥 ) · 𝑋 ) ↔ ( 𝑋 + 𝑋 ) = ( ( 𝑥 · 𝑋 ) + ( 𝑥 · 𝑋 ) ) ) )
14	7 13	syl5ibr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 · 𝑋 ) = 𝑋 → ( 𝑋 + 𝑋 ) = ( ( 𝑥 + 𝑥 ) · 𝑋 ) ) )
15	14	adantrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑥 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑥 ) = 𝑋 ) → ( 𝑋 + 𝑋 ) = ( ( 𝑥 + 𝑥 ) · 𝑋 ) ) )
16	15	reximdva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ( ( 𝑥 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 𝑥 ) = 𝑋 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 + 𝑋 ) = ( ( 𝑥 + 𝑥 ) · 𝑋 ) ) )
17	4 16	mpd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 + 𝑋 ) = ( ( 𝑥 + 𝑥 ) · 𝑋 ) )