Metamath Proof Explorer

Theorem rngoi

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007) (Proof shortened by Mario Carneiro, 21-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	rngoi	$⊢ R \in RingOps \to ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))$

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	opeq12i	$⊢ ⟨G, H⟩ = ⟨1^{st} (R), 2^{nd} (R)⟩$
5		relrngo	$⊢ Rel RingOps$
6		1st2nd	$⊢ (Rel RingOps \land R \in RingOps) \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
7	5 6	mpan	$⊢ R \in RingOps \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
8	4 7	eqtr4id	$⊢ R \in RingOps \to ⟨G, H⟩ = R$
9		id	$⊢ R \in RingOps \to R \in RingOps$
10	8 9	eqeltrd	$⊢ R \in RingOps \to ⟨G, H⟩ \in RingOps$
11	2	fvexi	$⊢ H \in V$
12	3	isrngo	$⊢ H \in V \to (⟨G, H⟩ \in RingOps \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))))$
13	11 12	ax-mp	$⊢ ⟨G, H⟩ \in RingOps \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))$
14	10 13	sylib	$⊢ R \in RingOps \to ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))$