Step | Hyp | Ref
| Expression |
1 | | simpll 763 |
. . 3
β’ (((π
β oRing β§ π β π΅) β§ 0 β€ π) β π
β oRing) |
2 | | simplr 765 |
. . 3
β’ (((π
β oRing β§ π β π΅) β§ 0 β€ π) β π β π΅) |
3 | | simpr 483 |
. . 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 32691 |
. . 3
β’ ((π
β oRing β§ (π β π΅ β§ 0 β€ π) β§ (π β π΅ β§ 0 β€ π)) β 0 β€ (π Β· π)) |
9 | 1, 2, 3, 2, 3, 8 | syl122anc 1377 |
. 2
β’ (((π
β oRing β§ π β π΅) β§ 0 β€ π) β 0 β€ (π Β· π)) |
10 | | simpll 763 |
. . . 4
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π
β oRing) |
11 | | orngring 32688 |
. . . . . . 7
β’ (π
β oRing β π
β Ring) |
12 | 11 | ad2antrr 722 |
. . . . . 6
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π
β Ring) |
13 | | ringgrp 20132 |
. . . . . 6
β’ (π
β Ring β π
β Grp) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π
β Grp) |
15 | | simplr 765 |
. . . . 5
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π β π΅) |
16 | | eqid 2730 |
. . . . . 6
β’
(invgβπ
) = (invgβπ
) |
17 | 4, 16 | grpinvcl 18908 |
. . . . 5
β’ ((π
β Grp β§ π β π΅) β ((invgβπ
)βπ) β π΅) |
18 | 14, 15, 17 | syl2anc 582 |
. . . 4
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β ((invgβπ
)βπ) β π΅) |
19 | | orngogrp 32689 |
. . . . . . . 8
β’ (π
β oRing β π
β oGrp) |
20 | | isogrp 32490 |
. . . . . . . . 9
β’ (π
β oGrp β (π
β Grp β§ π
β oMnd)) |
21 | 20 | simprbi 495 |
. . . . . . . 8
β’ (π
β oGrp β π
β oMnd) |
22 | 19, 21 | syl 17 |
. . . . . . 7
β’ (π
β oRing β π
β oMnd) |
23 | 10, 22 | syl 17 |
. . . . . 6
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π
β oMnd) |
24 | 4, 6 | grpidcl 18886 |
. . . . . . 7
β’ (π
β Grp β 0 β π΅) |
25 | 14, 24 | syl 17 |
. . . . . 6
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β 0 β π΅) |
26 | | simpl 481 |
. . . . . . . . . . 11
β’ ((π
β oRing β§ π β π΅) β π
β oRing) |
27 | 11, 13, 24 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π
β oRing β 0 β π΅) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((π
β oRing β§ π β π΅) β 0 β π΅) |
29 | | simpr 483 |
. . . . . . . . . . 11
β’ ((π
β oRing β§ π β π΅) β π β π΅) |
30 | 26, 28, 29 | 3jca 1126 |
. . . . . . . . . 10
β’ ((π
β oRing β§ π β π΅) β (π
β oRing β§ 0 β π΅ β§ π β π΅)) |
31 | | eqid 2730 |
. . . . . . . . . . . 12
β’
(ltβπ
) =
(ltβπ
) |
32 | 5, 31 | pltle 18290 |
. . . . . . . . . . 11
β’ ((π
β oRing β§ 0 β π΅ β§ π β π΅) β ( 0 (ltβπ
)π β 0 β€ π)) |
33 | 32 | con3dimp 407 |
. . . . . . . . . 10
β’ (((π
β oRing β§ 0 β π΅ β§ π β π΅) β§ Β¬ 0 β€ π) β Β¬ 0 (ltβπ
)π) |
34 | 30, 33 | sylan 578 |
. . . . . . . . 9
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β Β¬ 0 (ltβπ
)π) |
35 | | omndtos 32493 |
. . . . . . . . . . . . 13
β’ (π
β oMnd β π
β Toset) |
36 | 22, 35 | syl 17 |
. . . . . . . . . . . 12
β’ (π
β oRing β π
β Toset) |
37 | 4, 5, 31 | tosso 18376 |
. . . . . . . . . . . . . 14
β’ (π
β Toset β (π
β Toset β
((ltβπ
) Or π΅ β§ ( I βΎ π΅) β β€ ))) |
38 | 37 | ibi 266 |
. . . . . . . . . . . . 13
β’ (π
β Toset β
((ltβπ
) Or π΅ β§ ( I βΎ π΅) β β€ )) |
39 | 38 | simpld 493 |
. . . . . . . . . . . 12
β’ (π
β Toset β
(ltβπ
) Or π΅) |
40 | 10, 36, 39 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β (ltβπ
) Or π΅) |
41 | | solin 5612 |
. . . . . . . . . . 11
β’
(((ltβπ
) Or
π΅ β§ ( 0 β π΅ β§ π β π΅)) β ( 0 (ltβπ
)π β¨ 0 = π β¨ π(ltβπ
) 0 )) |
42 | 40, 25, 15, 41 | syl12anc 833 |
. . . . . . . . . 10
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β ( 0 (ltβπ
)π β¨ 0 = π β¨ π(ltβπ
) 0 )) |
43 | | 3orass 1088 |
. . . . . . . . . 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 885 |
. . . . . . . . 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 866 |
. . . . . . . . 9
β’ (( 0 = π β¨ π(ltβπ
) 0 ) β (π(ltβπ
) 0 β¨ 0 = π)) |
48 | | eqcom 2737 |
. . . . . . . . . 10
β’ ( 0 = π β π = 0 ) |
49 | 48 | orbi2i 909 |
. . . . . . . . 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 18377 |
. . . . . . . . 9
β’ (π
β Toset β π
β Poset) |
53 | 10, 36, 52 | 3syl 18 |
. . . . . . . 8
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π
β Poset) |
54 | 4, 5, 31 | pleval2 18294 |
. . . . . . . 8
β’ ((π
β Poset β§ π β π΅ β§ 0 β π΅) β (π β€ 0 β (π(ltβπ
) 0 β¨ π = 0 ))) |
55 | 53, 15, 25, 54 | syl3anc 1369 |
. . . . . . 7
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β (π β€ 0 β (π(ltβπ
) 0 β¨ π = 0 ))) |
56 | 51, 55 | mpbird 256 |
. . . . . 6
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β π β€ 0 ) |
57 | | eqid 2730 |
. . . . . . 7
β’
(+gβπ
) = (+gβπ
) |
58 | 4, 5, 57 | omndadd 32494 |
. . . . . 6
β’ ((π
β oMnd β§ (π β π΅ β§ 0 β π΅ β§ ((invgβπ
)βπ) β π΅) β§ π β€ 0 ) β (π(+gβπ
)((invgβπ
)βπ)) β€ ( 0 (+gβπ
)((invgβπ
)βπ))) |
59 | 23, 15, 25, 18, 56, 58 | syl131anc 1381 |
. . . . 5
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β (π(+gβπ
)((invgβπ
)βπ)) β€ ( 0 (+gβπ
)((invgβπ
)βπ))) |
60 | 4, 57, 6, 16 | grprinv 18911 |
. . . . . 6
β’ ((π
β Grp β§ π β π΅) β (π(+gβπ
)((invgβπ
)βπ)) = 0 ) |
61 | 14, 15, 60 | syl2anc 582 |
. . . . 5
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β (π(+gβπ
)((invgβπ
)βπ)) = 0 ) |
62 | 4, 57, 6 | grplid 18888 |
. . . . . 6
β’ ((π
β Grp β§
((invgβπ
)βπ) β π΅) β ( 0 (+gβπ
)((invgβπ
)βπ)) = ((invgβπ
)βπ)) |
63 | 14, 18, 62 | syl2anc 582 |
. . . . 5
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β ( 0 (+gβπ
)((invgβπ
)βπ)) = ((invgβπ
)βπ)) |
64 | 59, 61, 63 | 3brtr3d 5178 |
. . . 4
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β 0 β€
((invgβπ
)βπ)) |
65 | 4, 5, 6, 7 | orngmul 32691 |
. . . 4
β’ ((π
β oRing β§
(((invgβπ
)βπ) β π΅ β§ 0 β€
((invgβπ
)βπ)) β§ (((invgβπ
)βπ) β π΅ β§ 0 β€
((invgβπ
)βπ))) β 0 β€
(((invgβπ
)βπ) Β·
((invgβπ
)βπ))) |
66 | 10, 18, 64, 18, 64, 65 | syl122anc 1377 |
. . 3
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β 0 β€
(((invgβπ
)βπ) Β·
((invgβπ
)βπ))) |
67 | 4, 7, 16, 12, 15, 15 | ringm2neg 20194 |
. . 3
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β (((invgβπ
)βπ) Β·
((invgβπ
)βπ)) = (π Β· π)) |
68 | 66, 67 | breqtrd 5173 |
. 2
β’ (((π
β oRing β§ π β π΅) β§ Β¬ 0 β€ π) β 0 β€ (π Β· π)) |
69 | 9, 68 | pm2.61dan 809 |
1
β’ ((π
β oRing β§ π β π΅) β 0 β€ (π Β· π)) |