Proof of Theorem orngsqr
Step | Hyp | Ref
| Expression |
1 | | simpll 764 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝑅 ∈ oRing) |
2 | | simplr 766 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝑋 ∈ 𝐵) |
3 | | simpr 485 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 0 ≤ 𝑋) |
4 | | orngmul.0 |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
5 | | orngmul.1 |
. . . 4
⊢ ≤ =
(le‘𝑅) |
6 | | orngmul.2 |
. . . 4
⊢ 0 =
(0g‘𝑅) |
7 | | orngmul.3 |
. . . 4
⊢ · =
(.r‘𝑅) |
8 | 4, 5, 6, 7 | orngmul 31502 |
. . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋)) → 0 ≤ (𝑋 · 𝑋)) |
9 | 1, 2, 3, 2, 3, 8 | syl122anc 1378 |
. 2
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑋 · 𝑋)) |
10 | | simpll 764 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ oRing) |
11 | | orngring 31499 |
. . . . . . 7
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) |
12 | 11 | ad2antrr 723 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ Ring) |
13 | | ringgrp 19788 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ Grp) |
15 | | simplr 766 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑋 ∈ 𝐵) |
16 | | eqid 2738 |
. . . . . 6
⊢
(invg‘𝑅) = (invg‘𝑅) |
17 | 4, 16 | grpinvcl 18627 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((invg‘𝑅)‘𝑋) ∈ 𝐵) |
18 | 14, 15, 17 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ((invg‘𝑅)‘𝑋) ∈ 𝐵) |
19 | | orngogrp 31500 |
. . . . . . . 8
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) |
20 | | isogrp 31328 |
. . . . . . . . 9
⊢ (𝑅 ∈ oGrp ↔ (𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd)) |
21 | 20 | simprbi 497 |
. . . . . . . 8
⊢ (𝑅 ∈ oGrp → 𝑅 ∈ oMnd) |
22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oMnd) |
23 | 10, 22 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ oMnd) |
24 | 4, 6 | grpidcl 18607 |
. . . . . . 7
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
25 | 14, 24 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ∈ 𝐵) |
26 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ oRing) |
27 | 11, 13, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ oRing → 0 ∈ 𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ∈ 𝐵) |
29 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
30 | 26, 28, 29 | 3jca 1127 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → (𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
31 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(lt‘𝑅) =
(lt‘𝑅) |
32 | 5, 31 | pltle 18051 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ( 0 (lt‘𝑅)𝑋 → 0 ≤ 𝑋)) |
33 | 32 | con3dimp 409 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ¬ 0 (lt‘𝑅)𝑋) |
34 | 30, 33 | sylan 580 |
. . . . . . . . 9
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ¬ 0 (lt‘𝑅)𝑋) |
35 | | omndtos 31331 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ oMnd → 𝑅 ∈ Toset) |
36 | 22, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Toset) |
37 | 4, 5, 31 | tosso 18137 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Toset → (𝑅 ∈ Toset ↔
((lt‘𝑅) Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ))) |
38 | 37 | ibi 266 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Toset →
((lt‘𝑅) Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) |
39 | 38 | simpld 495 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Toset →
(lt‘𝑅) Or 𝐵) |
40 | 10, 36, 39 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (lt‘𝑅) Or 𝐵) |
41 | | solin 5528 |
. . . . . . . . . . 11
⊢
(((lt‘𝑅) Or
𝐵 ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ( 0 (lt‘𝑅)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 )) |
42 | 40, 25, 15, 41 | syl12anc 834 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 (lt‘𝑅)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 )) |
43 | | 3orass 1089 |
. . . . . . . . . 10
⊢ (( 0
(lt‘𝑅)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ) ↔ ( 0
(lt‘𝑅)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ))) |
44 | 42, 43 | sylib 217 |
. . . . . . . . 9
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 (lt‘𝑅)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ))) |
45 | | orel1 886 |
. . . . . . . . 9
⊢ (¬
0
(lt‘𝑅)𝑋 → (( 0 (lt‘𝑅)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 )) → ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ))) |
46 | 34, 44, 45 | sylc 65 |
. . . . . . . 8
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 )) |
47 | | orcom 867 |
. . . . . . . . 9
⊢ (( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ) ↔ (𝑋(lt‘𝑅) 0 ∨ 0 = 𝑋)) |
48 | | eqcom 2745 |
. . . . . . . . . 10
⊢ ( 0 = 𝑋 ↔ 𝑋 = 0 ) |
49 | 48 | orbi2i 910 |
. . . . . . . . 9
⊢ ((𝑋(lt‘𝑅) 0 ∨ 0 = 𝑋) ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 )) |
50 | 47, 49 | bitri 274 |
. . . . . . . 8
⊢ (( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ) ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 )) |
51 | 46, 50 | sylib 217 |
. . . . . . 7
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 )) |
52 | | tospos 18138 |
. . . . . . . . 9
⊢ (𝑅 ∈ Toset → 𝑅 ∈ Poset) |
53 | 10, 36, 52 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ Poset) |
54 | 4, 5, 31 | pleval2 18055 |
. . . . . . . 8
⊢ ((𝑅 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑋 ≤ 0 ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 ))) |
55 | 53, 15, 25, 54 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋 ≤ 0 ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 ))) |
56 | 51, 55 | mpbird 256 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑋 ≤ 0 ) |
57 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
58 | 4, 5, 57 | omndadd 31332 |
. . . . . 6
⊢ ((𝑅 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ((invg‘𝑅)‘𝑋) ∈ 𝐵) ∧ 𝑋 ≤ 0 ) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) ≤ ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋))) |
59 | 23, 15, 25, 18, 56, 58 | syl131anc 1382 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) ≤ ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋))) |
60 | 4, 57, 6, 16 | grprinv 18629 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) = 0 ) |
61 | 14, 15, 60 | syl2anc 584 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) = 0 ) |
62 | 4, 57, 6 | grplid 18609 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧
((invg‘𝑅)‘𝑋) ∈ 𝐵) → ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋)) = ((invg‘𝑅)‘𝑋)) |
63 | 14, 18, 62 | syl2anc 584 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋)) = ((invg‘𝑅)‘𝑋)) |
64 | 59, 61, 63 | 3brtr3d 5105 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ≤
((invg‘𝑅)‘𝑋)) |
65 | 4, 5, 6, 7 | orngmul 31502 |
. . . 4
⊢ ((𝑅 ∈ oRing ∧
(((invg‘𝑅)‘𝑋) ∈ 𝐵 ∧ 0 ≤
((invg‘𝑅)‘𝑋)) ∧ (((invg‘𝑅)‘𝑋) ∈ 𝐵 ∧ 0 ≤
((invg‘𝑅)‘𝑋))) → 0 ≤
(((invg‘𝑅)‘𝑋) ·
((invg‘𝑅)‘𝑋))) |
66 | 10, 18, 64, 18, 64, 65 | syl122anc 1378 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ≤
(((invg‘𝑅)‘𝑋) ·
((invg‘𝑅)‘𝑋))) |
67 | 4, 7, 16, 12, 15, 15 | ringm2neg 19837 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (((invg‘𝑅)‘𝑋) ·
((invg‘𝑅)‘𝑋)) = (𝑋 · 𝑋)) |
68 | 66, 67 | breqtrd 5100 |
. 2
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ≤ (𝑋 · 𝑋)) |
69 | 9, 68 | pm2.61dan 810 |
1
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋)) |