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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	orngmullt.t	⊢ · = ( .r ‘ 𝑅 )
	orngmullt.0	⊢ 0 = ( 0g ‘ 𝑅 )
	orngmullt.l	⊢ < = ( lt ‘ 𝑅 )
	orngmullt.1	⊢ ( 𝜑 → 𝑅 ∈ oRing )
	orngmullt.4	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	orngmullt.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	orngmullt.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	orngmullt.x	⊢ ( 𝜑 → 0 < 𝑋 )
	orngmullt.y	⊢ ( 𝜑 → 0 < 𝑌 )
Assertion	orngmullt	⊢ ( 𝜑 → 0 < ( 𝑋 · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		orngmullt.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		orngmullt.t	⊢ · = ( .r ‘ 𝑅 )
3		orngmullt.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		orngmullt.l	⊢ < = ( lt ‘ 𝑅 )
5		orngmullt.1	⊢ ( 𝜑 → 𝑅 ∈ oRing )
6		orngmullt.4	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
7		orngmullt.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		orngmullt.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		orngmullt.x	⊢ ( 𝜑 → 0 < 𝑋 )
10		orngmullt.y	⊢ ( 𝜑 → 0 < 𝑌 )
11		orngring	⊢ ( 𝑅 ∈ oRing → 𝑅 ∈ Ring )
12		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
13	1 3	grpidcl	⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
14	5 11 12 13	4syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
15		eqid	⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
16	15 4	pltval	⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ ( 0 ( le ‘ 𝑅 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
17	5 14 7 16	syl3anc	⊢ ( 𝜑 → ( 0 < 𝑋 ↔ ( 0 ( le ‘ 𝑅 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
18	9 17	mpbid	⊢ ( 𝜑 → ( 0 ( le ‘ 𝑅 ) 𝑋 ∧ 0 ≠ 𝑋 ) )
19	18	simpld	⊢ ( 𝜑 → 0 ( le ‘ 𝑅 ) 𝑋 )
20	15 4	pltval	⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 < 𝑌 ↔ ( 0 ( le ‘ 𝑅 ) 𝑌 ∧ 0 ≠ 𝑌 ) ) )
21	5 14 8 20	syl3anc	⊢ ( 𝜑 → ( 0 < 𝑌 ↔ ( 0 ( le ‘ 𝑅 ) 𝑌 ∧ 0 ≠ 𝑌 ) ) )
22	10 21	mpbid	⊢ ( 𝜑 → ( 0 ( le ‘ 𝑅 ) 𝑌 ∧ 0 ≠ 𝑌 ) )
23	22	simpld	⊢ ( 𝜑 → 0 ( le ‘ 𝑅 ) 𝑌 )
24	1 15 3 2	orngmul	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ( le ‘ 𝑅 ) 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ( le ‘ 𝑅 ) 𝑌 ) ) → 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
25	5 7 19 8 23 24	syl122anc	⊢ ( 𝜑 → 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
26	18	simprd	⊢ ( 𝜑 → 0 ≠ 𝑋 )
27	26	necomd	⊢ ( 𝜑 → 𝑋 ≠ 0 )
28	22	simprd	⊢ ( 𝜑 → 0 ≠ 𝑌 )
29	28	necomd	⊢ ( 𝜑 → 𝑌 ≠ 0 )
30	1 3 2 6 7 8	drngmulne0	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )
31	27 29 30	mpbir2and	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ≠ 0 )
32	31	necomd	⊢ ( 𝜑 → 0 ≠ ( 𝑋 · 𝑌 ) )
33	5 11	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
34	1 2	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
35	33 7 8 34	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
36	15 4	pltval	⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) → ( 0 < ( 𝑋 · 𝑌 ) ↔ ( 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ∧ 0 ≠ ( 𝑋 · 𝑌 ) ) ) )
37	5 14 35 36	syl3anc	⊢ ( 𝜑 → ( 0 < ( 𝑋 · 𝑌 ) ↔ ( 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ∧ 0 ≠ ( 𝑋 · 𝑌 ) ) ) )
38	25 32 37	mpbir2and	⊢ ( 𝜑 → 0 < ( 𝑋 · 𝑌 ) )