This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 
|- .x. = ( .r ` R )
orngmullt.0 
|- .0. = ( 0g ` R )
orngmullt.l 
|- .< = ( lt ` R )
orngmullt.1 
|- ( ph -> R e. oRing )
orngmullt.4 
|- ( ph -> R e. DivRing )
orngmullt.2 
|- ( ph -> X e. B )
orngmullt.3 
|- ( ph -> Y e. B )
orngmullt.x 
|- ( ph -> .0. .< X )
orngmullt.y 
|- ( ph -> .0. .< Y )
Assertion orngmullt 
|- ( ph -> .0. .< ( X .x. Y ) )

Proof

Step Hyp Ref Expression
1 orngmullt.b 
 |-  B = ( Base ` R )
2 orngmullt.t 
 |-  .x. = ( .r ` R )
3 orngmullt.0 
 |-  .0. = ( 0g ` R )
4 orngmullt.l 
 |-  .< = ( lt ` R )
5 orngmullt.1 
 |-  ( ph -> R e. oRing )
6 orngmullt.4 
 |-  ( ph -> R e. DivRing )
7 orngmullt.2 
 |-  ( ph -> X e. B )
8 orngmullt.3 
 |-  ( ph -> Y e. B )
9 orngmullt.x 
 |-  ( ph -> .0. .< X )
10 orngmullt.y 
 |-  ( ph -> .0. .< Y )
11 orngring 
 |-  ( R e. oRing -> R e. Ring )
12 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
13 1 3 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
14 5 11 12 13 4syl 
 |-  ( ph -> .0. e. B )
15 eqid 
 |-  ( le ` R ) = ( le ` R )
16 15 4 pltval 
 |-  ( ( R e. oRing /\ .0. e. B /\ X e. B ) -> ( .0. .< X <-> ( .0. ( le ` R ) X /\ .0. =/= X ) ) )
17 5 14 7 16 syl3anc 
 |-  ( ph -> ( .0. .< X <-> ( .0. ( le ` R ) X /\ .0. =/= X ) ) )
18 9 17 mpbid 
 |-  ( ph -> ( .0. ( le ` R ) X /\ .0. =/= X ) )
19 18 simpld 
 |-  ( ph -> .0. ( le ` R ) X )
20 15 4 pltval 
 |-  ( ( R e. oRing /\ .0. e. B /\ Y e. B ) -> ( .0. .< Y <-> ( .0. ( le ` R ) Y /\ .0. =/= Y ) ) )
21 5 14 8 20 syl3anc 
 |-  ( ph -> ( .0. .< Y <-> ( .0. ( le ` R ) Y /\ .0. =/= Y ) ) )
22 10 21 mpbid 
 |-  ( ph -> ( .0. ( le ` R ) Y /\ .0. =/= Y ) )
23 22 simpld 
 |-  ( ph -> .0. ( le ` R ) Y )
24 1 15 3 2 orngmul 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. ( le ` R ) X ) /\ ( Y e. B /\ .0. ( le ` R ) Y ) ) -> .0. ( le ` R ) ( X .x. Y ) )
25 5 7 19 8 23 24 syl122anc 
 |-  ( ph -> .0. ( le ` R ) ( X .x. Y ) )
26 18 simprd 
 |-  ( ph -> .0. =/= X )
27 26 necomd 
 |-  ( ph -> X =/= .0. )
28 22 simprd 
 |-  ( ph -> .0. =/= Y )
29 28 necomd 
 |-  ( ph -> Y =/= .0. )
30 1 3 2 6 7 8 drngmulne0 
 |-  ( ph -> ( ( X .x. Y ) =/= .0. <-> ( X =/= .0. /\ Y =/= .0. ) ) )
31 27 29 30 mpbir2and 
 |-  ( ph -> ( X .x. Y ) =/= .0. )
32 31 necomd 
 |-  ( ph -> .0. =/= ( X .x. Y ) )
33 5 11 syl 
 |-  ( ph -> R e. Ring )
34 1 2 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
35 33 7 8 34 syl3anc 
 |-  ( ph -> ( X .x. Y ) e. B )
36 15 4 pltval 
 |-  ( ( R e. oRing /\ .0. e. B /\ ( X .x. Y ) e. B ) -> ( .0. .< ( X .x. Y ) <-> ( .0. ( le ` R ) ( X .x. Y ) /\ .0. =/= ( X .x. Y ) ) ) )
37 5 14 35 36 syl3anc 
 |-  ( ph -> ( .0. .< ( X .x. Y ) <-> ( .0. ( le ` R ) ( X .x. Y ) /\ .0. =/= ( X .x. Y ) ) ) )
38 25 32 37 mpbir2and 
 |-  ( ph -> .0. .< ( X .x. Y ) )