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 \in RingOps \land A \in X) \to \exists x \in 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 \in RingOps \land A \in X) \to \exists x \in X (x H A = A \land A H x = A)$
5		oveq12	$⊢ (x H A = A \land x H A = A) \to (x H A) G (x H A) = A G A$
6	5	anidms	$⊢ x H A = A \to (x H A) G (x H A) = A G A$
7	6	eqcomd	$⊢ x H A = A \to A G A = (x H A) G (x H A)$
8		simpll	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to R \in RingOps$
9		simpr	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to x \in X$
10		simplr	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to A \in X$
11	1 2 3	rngodir	$⊢ (R \in RingOps \land (x \in X \land x \in X \land A \in X)) \to (x G x) H A = (x H A) G (x H A)$
12	8 9 9 10 11	syl13anc	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to (x G x) H A = (x H A) G (x H A)$
13	12	eqeq2d	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to (A G A = (x G x) H A \leftrightarrow A G A = (x H A) G (x H A))$
14	7 13	imbitrrid	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to (x H A = A \to A G A = (x G x) H A)$
15	14	adantrd	$⊢ ((R \in RingOps \land A \in X) \land x \in X) \to ((x H A = A \land A H x = A) \to A G A = (x G x) H A)$
16	15	reximdva	$⊢ (R \in RingOps \land A \in X) \to (\exists x \in X (x H A = A \land A H x = A) \to \exists x \in X A G A = (x G x) H A)$
17	4 16	mpd	$⊢ (R \in RingOps \land A \in X) \to \exists x \in X A G A = (x G x) H A$