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	26 11 13 24	4syl	$⊢ (R \in oRing \land X \in B) \to \underset{˙}{0} \in B$
28		simpr	$⊢ (R \in oRing \land X \in B) \to X \in B$
29	26 27 28	3jca	$⊢ (R \in oRing \land X \in B) \to (R \in oRing \land \underset{˙}{0} \in B \land X \in B)$
30		eqid	$⊢ <_{R} = <_{R}$
31	2 30	pltle	$⊢ (R \in oRing \land \underset{˙}{0} \in B \land X \in B) \to (\underset{˙}{0} <_{R} X \to \underset{˙}{0} \underset{˙}{\leq} X)$
32	31	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$
33	29 32	sylan	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \neg \underset{˙}{0} <_{R} X$
34		omndtos	$⊢ R \in oMnd \to R \in Toset$
35	1 2 30	tosso	$⊢ R \in Toset \to (R \in Toset \leftrightarrow (<_{R} Or B \land {I ↾}_{B} \subseteq \underset{˙}{\leq}))$
36	35	ibi	$⊢ R \in Toset \to (<_{R} Or B \land {I ↾}_{B} \subseteq \underset{˙}{\leq})$
37	36	simpld	$⊢ R \in Toset \to <_{R} Or B$
38	10 22 34 37	4syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to <_{R} Or B$
39		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})$
40	38 25 15 39	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})$
41		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}))$
42	40 41	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}))$
43		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}))$
44	33 42 43	sylc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0})$
45		orcom	$⊢ (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}) \leftrightarrow (X <_{R} \underset{˙}{0} \lor \underset{˙}{0} = X)$
46		eqcom	$⊢ \underset{˙}{0} = X \leftrightarrow X = \underset{˙}{0}$
47	46	orbi2i	$⊢ (X <_{R} \underset{˙}{0} \lor \underset{˙}{0} = X) \leftrightarrow (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0})$
48	45 47	bitri	$⊢ (\underset{˙}{0} = X \lor X <_{R} \underset{˙}{0}) \leftrightarrow (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0})$
49	44 48	sylib	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to (X <_{R} \underset{˙}{0} \lor X = \underset{˙}{0})$
50		tospos	$⊢ R \in Toset \to R \in Poset$
51	10 22 34 50	4syl	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to R \in Poset$
52	1 2 30	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}))$
53	51 15 25 52	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}))$
54	49 53	mpbird	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to X \underset{˙}{\leq} \underset{˙}{0}$
55		eqid	$⊢ +_{R} = +_{R}$
56	1 2 55	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))$
57	23 15 25 18 54 56	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))$
58	1 55 3 16	grprinv	$⊢ (R \in Grp \land X \in B) \to X +_{R} {inv}_{g} (R) (X) = \underset{˙}{0}$
59	14 15 58	syl2anc	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to X +_{R} {inv}_{g} (R) (X) = \underset{˙}{0}$
60	1 55 3	grplid	$⊢ (R \in Grp \land {inv}_{g} (R) (X) \in B) \to \underset{˙}{0} +_{R} {inv}_{g} (R) (X) = {inv}_{g} (R) (X)$
61	14 18 60	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)$
62	57 59 61	3brtr3d	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} {inv}_{g} (R) (X)$
63	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))$
64	10 18 62 18 62 63	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))$
65	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$
66	64 65	breqtrd	$⊢ ((R \in oRing \land X \in B) \land \neg \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$
67	9 66	pm2.61dan	$⊢ (R \in oRing \land X \in B) \to \underset{˙}{0} \underset{˙}{\leq} (X \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem orngsqr

Proof