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 ⊢ G = 1 st ⁡ R
ringi.2 ⊢ H = 2 nd ⁡ R
ringi.3 ⊢ X = ran ⁡ G
Assertion rngo2 ⊢ R ∈ RingOps ∧ A ∈ X → ∃ x ∈ X A G A = x G x H A

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢ G = 1 st ⁡ R
2 ringi.2 ⊢ H = 2 nd ⁡ R
3 ringi.3 ⊢ X = ran ⁡ G
4 1 2 3 rngoid ⊢ R ∈ RingOps ∧ A ∈ X → ∃ x ∈ X x H A = A ∧ A H x = A
5 oveq12 ⊢ x H A = A ∧ x H A = A → x H A G x H A = A G A
6 5 anidms ⊢ x H A = A → x H A G x H A = A G A
7 6 eqcomd ⊢ x H A = A → A G A = x H A G x H A
8 simpll ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → R ∈ RingOps
9 simpr ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → x ∈ X
10 simplr ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → A ∈ X
11 1 2 3 rngodir ⊢ R ∈ RingOps ∧ x ∈ X ∧ x ∈ X ∧ A ∈ X → x G x H A = x H A G x H A
12 8 9 9 10 11 syl13anc ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → x G x H A = x H A G x H A
13 12 eqeq2d ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → A G A = x G x H A ↔ A G A = x H A G x H A
14 7 13 syl5ibr ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → x H A = A → A G A = x G x H A
15 14 adantrd ⊢ R ∈ RingOps ∧ A ∈ X ∧ x ∈ X → x H A = A ∧ A H x = A → A G A = x G x H A
16 15 reximdva ⊢ R ∈ RingOps ∧ A ∈ X → ∃ x ∈ X x H A = A ∧ A H x = A → ∃ x ∈ X A G A = x G x H A
17 4 16 mpd ⊢ R ∈ RingOps ∧ A ∈ X → ∃ x ∈ X A G A = x G x H A