orngmullt

Description: In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	orngmullt.b	$⊢ B = {Base}_{R}$
	orngmullt.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	orngmullt.0	$⊢ \underset{˙}{0} = 0_{R}$
	orngmullt.l	$⊢ \underset{˙}{<} = <_{R}$
	orngmullt.1	$⊢ φ \to R \in oRing$
	orngmullt.4	$⊢ φ \to R \in DivRing$
	orngmullt.2	$⊢ φ \to X \in B$
	orngmullt.3	$⊢ φ \to Y \in B$
	orngmullt.x	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} X$
	orngmullt.y	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} Y$
Assertion	orngmullt	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} (X \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		orngmullt.b	$⊢ B = {Base}_{R}$
2		orngmullt.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		orngmullt.0	$⊢ \underset{˙}{0} = 0_{R}$
4		orngmullt.l	$⊢ \underset{˙}{<} = <_{R}$
5		orngmullt.1	$⊢ φ \to R \in oRing$
6		orngmullt.4	$⊢ φ \to R \in DivRing$
7		orngmullt.2	$⊢ φ \to X \in B$
8		orngmullt.3	$⊢ φ \to Y \in B$
9		orngmullt.x	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} X$
10		orngmullt.y	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} Y$
11		orngring	$⊢ R \in oRing \to R \in Ring$
12		ringgrp	$⊢ R \in Ring \to R \in Grp$
13	1 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
14	5 11 12 13	4syl	$⊢ φ \to \underset{˙}{0} \in B$
15		eqid	$⊢ \leq_{R} = \leq_{R}$
16	15 4	pltval	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land X \in B) \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow (\underset{˙}{0} \leq_{R} X \land \underset{˙}{0} \neq X))$
17	5 14 7 16	syl3anc	$⊢ φ \to (\underset{˙}{0} \underset{˙}{<} X \leftrightarrow (\underset{˙}{0} \leq_{R} X \land \underset{˙}{0} \neq X))$
18	9 17	mpbid	$⊢ φ \to (\underset{˙}{0} \leq_{R} X \land \underset{˙}{0} \neq X)$
19	18	simpld	$⊢ φ \to \underset{˙}{0} \leq_{R} X$
20	15 4	pltval	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land Y \in B) \to (\underset{˙}{0} \underset{˙}{<} Y \leftrightarrow (\underset{˙}{0} \leq_{R} Y \land \underset{˙}{0} \neq Y))$
21	5 14 8 20	syl3anc	$⊢ φ \to (\underset{˙}{0} \underset{˙}{<} Y \leftrightarrow (\underset{˙}{0} \leq_{R} Y \land \underset{˙}{0} \neq Y))$
22	10 21	mpbid	$⊢ φ \to (\underset{˙}{0} \leq_{R} Y \land \underset{˙}{0} \neq Y)$
23	22	simpld	$⊢ φ \to \underset{˙}{0} \leq_{R} Y$
24	1 15 3 2	orngmul	$⊢ (R \in oRing \land (X \in B \land \underset{˙}{0} \leq_{R} X) \land (Y \in B \land \underset{˙}{0} \leq_{R} Y)) \to \underset{˙}{0} \leq_{R} (X \underset{˙}{\cdot} Y)$
25	5 7 19 8 23 24	syl122anc	$⊢ φ \to \underset{˙}{0} \leq_{R} (X \underset{˙}{\cdot} Y)$
26	18	simprd	$⊢ φ \to \underset{˙}{0} \neq X$
27	26	necomd	$⊢ φ \to X \neq \underset{˙}{0}$
28	22	simprd	$⊢ φ \to \underset{˙}{0} \neq Y$
29	28	necomd	$⊢ φ \to Y \neq \underset{˙}{0}$
30	1 3 2 6 7 8	drngmulne0	$⊢ φ \to (X \underset{˙}{\cdot} Y \neq \underset{˙}{0} \leftrightarrow (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}))$
31	27 29 30	mpbir2and	$⊢ φ \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$
32	31	necomd	$⊢ φ \to \underset{˙}{0} \neq X \underset{˙}{\cdot} Y$
33	5 11	syl	$⊢ φ \to R \in Ring$
34	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
35	33 7 8 34	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
36	15 4	pltval	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land X \underset{˙}{\cdot} Y \in B) \to (\underset{˙}{0} \underset{˙}{<} (X \underset{˙}{\cdot} Y) \leftrightarrow (\underset{˙}{0} \leq_{R} (X \underset{˙}{\cdot} Y) \land \underset{˙}{0} \neq X \underset{˙}{\cdot} Y))$
37	5 14 35 36	syl3anc	$⊢ φ \to (\underset{˙}{0} \underset{˙}{<} (X \underset{˙}{\cdot} Y) \leftrightarrow (\underset{˙}{0} \leq_{R} (X \underset{˙}{\cdot} Y) \land \underset{˙}{0} \neq X \underset{˙}{\cdot} Y))$
38	25 32 37	mpbir2and	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} (X \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem orngmullt

Proof