Proof of Theorem orngsqr
Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝑅 ∈ oRing) |
2 | | simplr 769 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝑋 ∈ 𝐵) |
3 | | simpr 488 |
. . 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 31082 |
. . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋)) → 0 ≤ (𝑋 · 𝑋)) |
9 | 1, 2, 3, 2, 3, 8 | syl122anc 1380 |
. 2
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑋 · 𝑋)) |
10 | | simpll 767 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ oRing) |
11 | | orngring 31079 |
. . . . . . 7
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) |
12 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ Ring) |
13 | | ringgrp 19424 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ Grp) |
15 | | simplr 769 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑋 ∈ 𝐵) |
16 | | eqid 2739 |
. . . . . 6
⊢
(invg‘𝑅) = (invg‘𝑅) |
17 | 4, 16 | grpinvcl 18272 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((invg‘𝑅)‘𝑋) ∈ 𝐵) |
18 | 14, 15, 17 | syl2anc 587 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ((invg‘𝑅)‘𝑋) ∈ 𝐵) |
19 | | orngogrp 31080 |
. . . . . . . 8
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) |
20 | | isogrp 30908 |
. . . . . . . . 9
⊢ (𝑅 ∈ oGrp ↔ (𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd)) |
21 | 20 | simprbi 500 |
. . . . . . . 8
⊢ (𝑅 ∈ oGrp → 𝑅 ∈ oMnd) |
22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oMnd) |
23 | 10, 22 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ oMnd) |
24 | 4, 6 | grpidcl 18252 |
. . . . . . 7
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
25 | 14, 24 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ∈ 𝐵) |
26 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ oRing) |
27 | 11, 13, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ oRing → 0 ∈ 𝐵) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ∈ 𝐵) |
29 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
30 | 26, 28, 29 | 3jca 1129 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → (𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
31 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(lt‘𝑅) =
(lt‘𝑅) |
32 | 5, 31 | pltle 17690 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ( 0 (lt‘𝑅)𝑋 → 0 ≤ 𝑋)) |
33 | 32 | con3dimp 412 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ¬ 0 (lt‘𝑅)𝑋) |
34 | 30, 33 | sylan 583 |
. . . . . . . . 9
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ¬ 0 (lt‘𝑅)𝑋) |
35 | | omndtos 30911 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ oMnd → 𝑅 ∈ Toset) |
36 | 22, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Toset) |
37 | 4, 5, 31 | tosso 17765 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Toset → (𝑅 ∈ Toset ↔
((lt‘𝑅) Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ))) |
38 | 37 | ibi 270 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Toset →
((lt‘𝑅) Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) |
39 | 38 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Toset →
(lt‘𝑅) Or 𝐵) |
40 | 10, 36, 39 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (lt‘𝑅) Or 𝐵) |
41 | | solin 5468 |
. . . . . . . . . . 11
⊢
(((lt‘𝑅) Or
𝐵 ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ( 0 (lt‘𝑅)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 )) |
42 | 40, 25, 15, 41 | syl12anc 836 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 (lt‘𝑅)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 )) |
43 | | 3orass 1091 |
. . . . . . . . . 10
⊢ (( 0
(lt‘𝑅)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ) ↔ ( 0
(lt‘𝑅)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ))) |
44 | 42, 43 | sylib 221 |
. . . . . . . . 9
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 (lt‘𝑅)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ))) |
45 | | orel1 888 |
. . . . . . . . 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 869 |
. . . . . . . . 9
⊢ (( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ) ↔ (𝑋(lt‘𝑅) 0 ∨ 0 = 𝑋)) |
48 | | eqcom 2746 |
. . . . . . . . . 10
⊢ ( 0 = 𝑋 ↔ 𝑋 = 0 ) |
49 | 48 | orbi2i 912 |
. . . . . . . . 9
⊢ ((𝑋(lt‘𝑅) 0 ∨ 0 = 𝑋) ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 )) |
50 | 47, 49 | bitri 278 |
. . . . . . . 8
⊢ (( 0 = 𝑋 ∨ 𝑋(lt‘𝑅) 0 ) ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 )) |
51 | 46, 50 | sylib 221 |
. . . . . . 7
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 )) |
52 | | tospos 30821 |
. . . . . . . . 9
⊢ (𝑅 ∈ Toset → 𝑅 ∈ Poset) |
53 | 10, 36, 52 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑅 ∈ Poset) |
54 | 4, 5, 31 | pleval2 17694 |
. . . . . . . 8
⊢ ((𝑅 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵) → (𝑋 ≤ 0 ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 ))) |
55 | 53, 15, 25, 54 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋 ≤ 0 ↔ (𝑋(lt‘𝑅) 0 ∨ 𝑋 = 0 ))) |
56 | 51, 55 | mpbird 260 |
. . . . . 6
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 𝑋 ≤ 0 ) |
57 | | eqid 2739 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
58 | 4, 5, 57 | omndadd 30912 |
. . . . . 6
⊢ ((𝑅 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ((invg‘𝑅)‘𝑋) ∈ 𝐵) ∧ 𝑋 ≤ 0 ) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) ≤ ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋))) |
59 | 23, 15, 25, 18, 56, 58 | syl131anc 1384 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) ≤ ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋))) |
60 | 4, 57, 6, 16 | grprinv 18274 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) = 0 ) |
61 | 14, 15, 60 | syl2anc 587 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (𝑋(+g‘𝑅)((invg‘𝑅)‘𝑋)) = 0 ) |
62 | 4, 57, 6 | grplid 18254 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧
((invg‘𝑅)‘𝑋) ∈ 𝐵) → ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋)) = ((invg‘𝑅)‘𝑋)) |
63 | 14, 18, 62 | syl2anc 587 |
. . . . 5
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → ( 0 (+g‘𝑅)((invg‘𝑅)‘𝑋)) = ((invg‘𝑅)‘𝑋)) |
64 | 59, 61, 63 | 3brtr3d 5062 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ≤
((invg‘𝑅)‘𝑋)) |
65 | 4, 5, 6, 7 | orngmul 31082 |
. . . 4
⊢ ((𝑅 ∈ oRing ∧
(((invg‘𝑅)‘𝑋) ∈ 𝐵 ∧ 0 ≤
((invg‘𝑅)‘𝑋)) ∧ (((invg‘𝑅)‘𝑋) ∈ 𝐵 ∧ 0 ≤
((invg‘𝑅)‘𝑋))) → 0 ≤
(((invg‘𝑅)‘𝑋) ·
((invg‘𝑅)‘𝑋))) |
66 | 10, 18, 64, 18, 64, 65 | syl122anc 1380 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ≤
(((invg‘𝑅)‘𝑋) ·
((invg‘𝑅)‘𝑋))) |
67 | 4, 7, 16, 12, 15, 15 | ringm2neg 19473 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → (((invg‘𝑅)‘𝑋) ·
((invg‘𝑅)‘𝑋)) = (𝑋 · 𝑋)) |
68 | 66, 67 | breqtrd 5057 |
. 2
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) ∧ ¬ 0 ≤ 𝑋) → 0 ≤ (𝑋 · 𝑋)) |
69 | 9, 68 | pm2.61dan 813 |
1
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋)) |