orngsqr

Description: In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018)

	Ref	Expression
Hypotheses	orngmul.0	$⊢ B = {Base}_{R}$
	orngmul.1	$⊢ \underset{˙}{\leq} = \leq_{R}$
	orngmul.2	$⊢ \underset{˙}{0} = 0_{R}$
	orngmul.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	orngsqr	$⊢ (R \in oRing \land X \in B) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		orngmul.0	$⊢ B = {Base}_{R}$
2		orngmul.1	$⊢ \underset{˙}{\leq} = \leq_{R}$
3		orngmul.2	$⊢ \underset{˙}{0} = 0_{R}$
4		orngmul.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		simpll	$⊢ ((R \in oRing \land X \in B) \land \underset{˙}{0} \underset{˙}{\leq} X) \to R \in oRing$
6		simplr	$⊢ ((R \in oRing \land X \in B) \land \underset{˙}{0} \underset{˙}{\leq} X) \to X \in B$
7		simpr	$⊢ ((R \in oRing \land X \in B) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} X$
8	1 2 3 4	orngmul	$⊢ (R \in oRing \land (X \in B \land \underset{˙}{0} \underset{˙}{\leq} X) \land (X \in B \land \underset{˙}{0} \underset{˙}{\leq} X)) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$
9	5 6 7 6 7 8	syl122anc	$⊢ ((R \in oRing \land X \in B) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$
10		simpll	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to R \in oRing$
11		orngring	$⊢ R \in oRing \to R \in Ring$
12	11	ad2antrr	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to R \in Ring$
13		ringgrp	$⊢ R \in Ring \to R \in Grp$
14	12 13	syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to R \in Grp$
15		simplr	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to X \in B$
16		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
17	1 16	grpinvcl	$⊢ (R \in Grp \land X \in B) \to {inv}_{g} (R) (X) \in B$
18	14 15 17	syl2anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to {inv}_{g} (R) (X) \in B$
19		orngogrp	$⊢ R \in oRing \to R \in oGrp$
20		isogrp	$⊢ R \in oGrp \leftrightarrow (R \in Grp \land R \in oMnd)$
21	20	simprbi	$⊢ R \in oGrp \to R \in oMnd$
22	19 21	syl	$⊢ R \in oRing \to R \in oMnd$
23	10 22	syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to R \in oMnd$
24	1 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
25	14 24	syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \in B$
26		simpl	$⊢ (R \in oRing \land X \in B) \to R \in oRing$
27	11 13 24	3syl	$⊢ R \in oRing \to \underset{˙}{0} \in B$
28	26 27	syl	$⊢ (R \in oRing \land X \in B) \to \underset{˙}{0} \in B$
29		simpr	$⊢ (R \in oRing \land X \in B) \to X \in B$
30	26 28 29	3jca	$⊢ (R \in oRing \land X \in B) \to (R \in oRing \land \underset{˙}{0} \in B \land X \in B)$
31		eqid	$⊢ <_{R} = <_{R}$
32	2 31	pltle	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land X \in B) \to (\underset{˙}{0} <_{R} X \to \underset{˙}{0} \underset{˙}{\leq} X)$
33	32	con3dimp	$⊢ ((R \in oRing \land \underset{˙}{0} \in B \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \neg \underset{˙}{0} <_{R} X$
34	30 33	sylan	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \neg \underset{˙}{0} <_{R} X$
35		omndtos	$⊢ R \in oMnd \to R \in Toset$
36	22 35	syl	$⊢ R \in oRing \to R \in Toset$
37	1 2 31	tosso	$⊢ R \in Toset \to (R \in Toset \leftrightarrow (<_{R} Or B \land {I ↾}_{B} \subseteq \underset{˙}{\leq}))$
38	37	ibi	$⊢ R \in Toset \to (<_{R} Or B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})$
39	38	simpld	$⊢ R \in Toset \to <_{R} Or B$
40	10 36 39	3syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to <_{R} Or B$
41		solin	$⊢ (<_{R} Or B \land (\underset{˙}{0} \in B \land X \in B)) \to (\underset{˙}{0} <_{R} X \lor \underset{˙}{0} = X \lor X <_{R} \underset{˙}{0})$
42	40 25 15 41	syl12anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (\underset{˙}{0} <_{R} X \lor \underset{˙}{0} = X \lor X <_{R} \underset{˙}{0})$
43		3orass	$⊢ (\underset{˙}{0} <_{R} X \lor \underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}) \leftrightarrow (\underset{˙}{0} <_{R} X \lor (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}))$
44	42 43	sylib	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (\underset{˙}{0} <_{R} X \lor (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}))$
45		orel1	$⊢ \neg \underset{˙}{0} <_{R} X \to ((\underset{˙}{0} <_{R} X \lor (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0})) \to (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}))$
46	34 44 45	sylc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0})$
47		orcom	$⊢ (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}) \leftrightarrow (X <_{R} \underset{˙}{0} \lor \underset{˙}{0} = X)$
48		eqcom	$⊢ \underset{˙}{0} = X \leftrightarrow X = \underset{˙}{0}$
49	48	orbi2i	$⊢ (X <_{R} \underset{˙}{0} \lor \underset{˙}{0} = X) \leftrightarrow (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0})$
50	47 49	bitri	$⊢ (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}) \leftrightarrow (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0})$
51	46 50	sylib	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0})$
52		tospos	$⊢ R \in Toset \to R \in Poset$
53	10 36 52	3syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to R \in Poset$
54	1 2 31	pleval2	$⊢ (R \in Poset \land X \in B \land \underset{˙}{0} \in B) \to (X \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0}))$
55	53 15 25 54	syl3anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (X \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0}))$
56	51 55	mpbird	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to X \underset{˙}{\leq} \underset{˙}{0}$
57		eqid	$⊢ +_{R} = +_{R}$
58	1 2 57	omndadd	$⊢ (R \in oMnd \land (X \in B \land \underset{˙}{0} \in B \land {inv}_{g} (R) (X) \in B) \land X \underset{˙}{\leq} \underset{˙}{0}) \to (X +_{R} {inv}_{g} (R) (X)) \underset{˙}{\leq} (\underset{˙}{0} +_{R} {inv}_{g} (R) (X))$
59	23 15 25 18 56 58	syl131anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (X +_{R} {inv}_{g} (R) (X)) \underset{˙}{\leq} (\underset{˙}{0} +_{R} {inv}_{g} (R) (X))$
60	1 57 3 16	grprinv	$⊢ (R \in Grp \land X \in B) \to X +_{R} {inv}_{g} (R) (X) = \underset{˙}{0}$
61	14 15 60	syl2anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to X +_{R} {inv}_{g} (R) (X) = \underset{˙}{0}$
62	1 57 3	grplid	$⊢ (R \in Grp \land {inv}_{g} (R) (X) \in B) \to \underset{˙}{0} +_{R} {inv}_{g} (R) (X) = {inv}_{g} (R) (X)$
63	14 18 62	syl2anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} +_{R} {inv}_{g} (R) (X) = {inv}_{g} (R) (X)$
64	59 61 63	3brtr3d	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} {inv}_{g} (R) (X)$
65	1 2 3 4	orngmul	$⊢ (R \in oRing \land ({inv}_{g} (R) (X) \in B \land \underset{˙}{0} \underset{˙}{\leq} {inv}_{g} (R) (X)) \land ({inv}_{g} (R) (X) \in B \land \underset{˙}{0} \underset{˙}{\leq} {inv}_{g} (R) (X))) \to \underset{˙}{0} \underset{˙}{\leq} ({inv}_{g} (R) (X) \underset{˙}{\cdot} {inv}_{g} (R) (X))$
66	10 18 64 18 64 65	syl122anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} ({inv}_{g} (R) (X) \underset{˙}{\cdot} {inv}_{g} (R) (X))$
67	1 4 16 12 15 15	ringm2neg	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to {inv}_{g} (R) (X) \underset{˙}{\cdot} {inv}_{g} (R) (X) = X \underset{˙}{\cdot} X$
68	66 67	breqtrd	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$
69	9 68	pm2.61dan	$⊢ (R \in oRing \land X \in B) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem orngsqr

Proof