rngomndo

Description: In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	unmnd.1	$⊢ H = 2^{nd} (R)$
	Assertion	rngomndo	$⊢ R \in RingOps \to H \in MndOp$

Proof

Step	Hyp	Ref	Expression
1		unmnd.1	$⊢ H = 2^{nd} (R)$
2		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
3		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
4	2 1 3	rngosm	$⊢ R \in RingOps \to H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R)$
5	2 1 3	rngoass	$⊢ (R \in RingOps \land (x \in ran 1^{st} (R) \land y \in ran 1^{st} (R) \land z \in ran 1^{st} (R))) \to (x H y) H z = x H (y H z)$
6	5	ralrimivvva	$⊢ R \in RingOps \to \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z)$
7	2 1 3	rngoi	$⊢ R \in RingOps \to ((1^{st} (R) \in AbelOp \land H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R)) \land (\forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) ((x H y) H z = x H (y H z) \land x H (y 1^{st} (R) z) = (x H y) 1^{st} (R) (x H z) \land (x 1^{st} (R) y) H z = (x H z) 1^{st} (R) (y H z)) \land \exists x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y)))$
8	7	simprrd	$⊢ R \in RingOps \to \exists x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y)$
9	1 2	rngorn1	$⊢ R \in RingOps \to ran 1^{st} (R) = dom dom H$
10		xpid11	$⊢ dom dom H \times dom dom H = ran 1^{st} (R) \times ran 1^{st} (R) \leftrightarrow dom dom H = ran 1^{st} (R)$
11	10	biimpri	$⊢ dom dom H = ran 1^{st} (R) \to dom dom H \times dom dom H = ran 1^{st} (R) \times ran 1^{st} (R)$
12		feq23	$⊢ (dom dom H \times dom dom H = ran 1^{st} (R) \times ran 1^{st} (R) \land dom dom H = ran 1^{st} (R)) \to (H : dom dom H \times dom dom H ⟶ dom dom H \leftrightarrow H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R))$
13	11 12	mpancom	$⊢ dom dom H = ran 1^{st} (R) \to (H : dom dom H \times dom dom H ⟶ dom dom H \leftrightarrow H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R))$
14		raleq	$⊢ dom dom H = ran 1^{st} (R) \to (\forall z \in dom dom H (x H y) H z = x H (y H z) \leftrightarrow \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z))$
15	14	raleqbi1dv	$⊢ dom dom H = ran 1^{st} (R) \to (\forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \leftrightarrow \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z))$
16	15	raleqbi1dv	$⊢ dom dom H = ran 1^{st} (R) \to (\forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \leftrightarrow \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z))$
17		raleq	$⊢ dom dom H = ran 1^{st} (R) \to (\forall y \in dom dom H (x H y = y \land y H x = y) \leftrightarrow \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y))$
18	17	rexeqbi1dv	$⊢ dom dom H = ran 1^{st} (R) \to (\exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y) \leftrightarrow \exists x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y))$
19	13 16 18	3anbi123d	$⊢ dom dom H = ran 1^{st} (R) \to ((H : dom dom H \times dom dom H ⟶ dom dom H \land \forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \land \exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y)) \leftrightarrow (H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R) \land \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z) \land \exists x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y)))$
20	19	eqcoms	$⊢ ran 1^{st} (R) = dom dom H \to ((H : dom dom H \times dom dom H ⟶ dom dom H \land \forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \land \exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y)) \leftrightarrow (H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R) \land \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z) \land \exists x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y)))$
21	9 20	syl	$⊢ R \in RingOps \to ((H : dom dom H \times dom dom H ⟶ dom dom H \land \forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \land \exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y)) \leftrightarrow (H : ran 1^{st} (R) \times ran 1^{st} (R) ⟶ ran 1^{st} (R) \land \forall x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) \forall z \in ran 1^{st} (R) (x H y) H z = x H (y H z) \land \exists x \in ran 1^{st} (R) \forall y \in ran 1^{st} (R) (x H y = y \land y H x = y)))$
22	4 6 8 21	mpbir3and	$⊢ R \in RingOps \to (H : dom dom H \times dom dom H ⟶ dom dom H \land \forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \land \exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y))$
23		fvex	$⊢ 2^{nd} (R) \in V$
24		eleq1	$⊢ H = 2^{nd} (R) \to (H \in V \leftrightarrow 2^{nd} (R) \in V)$
25	23 24	mpbiri	$⊢ H = 2^{nd} (R) \to H \in V$
26		eqid	$⊢ dom dom H = dom dom H$
27	26	ismndo1	$⊢ H \in V \to (H \in MndOp \leftrightarrow (H : dom dom H \times dom dom H ⟶ dom dom H \land \forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \land \exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y)))$
28	1 25 27	mp2b	$⊢ H \in MndOp \leftrightarrow (H : dom dom H \times dom dom H ⟶ dom dom H \land \forall x \in dom dom H \forall y \in dom dom H \forall z \in dom dom H (x H y) H z = x H (y H z) \land \exists x \in dom dom H \forall y \in dom dom H (x H y = y \land y H x = y))$
29	22 28	sylibr	$⊢ R \in RingOps \to H \in MndOp$

Metamath Proof Explorer

Theorem rngomndo

Proof