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	\|- .<_ = ( le ` R )
	orngmul.2	\|- .0. = ( 0g ` R )
	orngmul.3	\|- .x. = ( .r ` R )
Assertion	orngsqr	\|- ( ( R e. oRing /\ X e. B ) -> .0. .<_ ( X .x. X ) )

Proof

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

Metamath Proof Explorer

Theorem orngsqr

Proof