iscrngo2

Description: The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010)

	Ref	Expression
Hypotheses	iscring2.1	$⊢ G = 1^{st} (R)$
	iscring2.2	$⊢ H = 2^{nd} (R)$
	iscring2.3	$⊢ X = ran G$
Assertion	iscrngo2	$⊢ R \in CRingOps \leftrightarrow (R \in RingOps \land \forall x \in X \forall y \in X x H y = y H x)$

Proof

Step	Hyp	Ref	Expression
1		iscring2.1	$⊢ G = 1^{st} (R)$
2		iscring2.2	$⊢ H = 2^{nd} (R)$
3		iscring2.3	$⊢ X = ran G$
4		iscrngo	$⊢ R \in CRingOps \leftrightarrow (R \in RingOps \land R \in Com2)$
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		eleq1	$⊢ R = ⟨1^{st} (R), 2^{nd} (R)⟩ \to (R \in Com2 \leftrightarrow ⟨1^{st} (R), 2^{nd} (R)⟩ \in Com2)$
9	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
10	3 9	eqtri	$⊢ X = ran 1^{st} (R)$
11	10	raleqi	$⊢ \forall x \in X \forall y \in ran 1^{st} (R) x 2^{nd} (R) y = y 2^{nd} (R) x \leftrightarrow \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) x 2^{nd} (R) y = y 2^{nd} (R) x$
12	2	oveqi	$⊢ x H y = x 2^{nd} (R) y$
13	2	oveqi	$⊢ y H x = y 2^{nd} (R) x$
14	12 13	eqeq12i	$⊢ x H y = y H x \leftrightarrow x 2^{nd} (R) y = y 2^{nd} (R) x$
15	10 14	raleqbii	$⊢ \forall y \in X x H y = y H x \leftrightarrow \forall y \in ran 1^{st} (R) x 2^{nd} (R) y = y 2^{nd} (R) x$
16	15	ralbii	$⊢ \forall x \in X \forall y \in X x H y = y H x \leftrightarrow \forall x \in X \forall y \in ran 1^{st} (R) x 2^{nd} (R) y = y 2^{nd} (R) x$
17		fvex	$⊢ 1^{st} (R) \in V$
18		fvex	$⊢ 2^{nd} (R) \in V$
19		iscom2	$⊢ (1^{st} (R) \in V \land 2^{nd} (R) \in V) \to (⟨1^{st} (R), 2^{nd} (R)⟩ \in Com2 \leftrightarrow \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) x 2^{nd} (R) y = y 2^{nd} (R) x)$
20	17 18 19	mp2an	$⊢ ⟨1^{st} (R), 2^{nd} (R)⟩ \in Com2 \leftrightarrow \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) x 2^{nd} (R) y = y 2^{nd} (R) x$
21	11 16 20	3bitr4ri	$⊢ ⟨1^{st} (R), 2^{nd} (R)⟩ \in Com2 \leftrightarrow \forall x \in X \forall y \in X x H y = y H x$
22	8 21	bitrdi	$⊢ R = ⟨1^{st} (R), 2^{nd} (R)⟩ \to (R \in Com2 \leftrightarrow \forall x \in X \forall y \in X x H y = y H x)$
23	7 22	syl	$⊢ R \in RingOps \to (R \in Com2 \leftrightarrow \forall x \in X \forall y \in X x H y = y H x)$
24	23	pm5.32i	$⊢ (R \in RingOps \land R \in Com2) \leftrightarrow (R \in RingOps \land \forall x \in X \forall y \in X x H y = y H x)$
25	4 24	bitri	$⊢ R \in CRingOps \leftrightarrow (R \in RingOps \land \forall x \in X \forall y \in X x H y = y H x)$

Metamath Proof Explorer

Theorem iscrngo2

Proof