Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . 3
⊢ (𝑅 ∈ (Ring ∩ oGrp) ↔
(𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp)) |
2 | 1 | anbi1i 727 |
. 2
⊢ ((𝑅 ∈ (Ring ∩ oGrp) ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
3 | | fvex 6113 |
. . . . . 6
⊢
(.r‘𝑟) ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑟 = 𝑅 → (.r‘𝑟) ∈ V) |
5 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → 𝑡 = (.r‘𝑟)) |
6 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → 𝑟 = 𝑅) |
7 | 6 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → (.r‘𝑟) = (.r‘𝑅)) |
8 | | isorng.2 |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
9 | 7, 8 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → (.r‘𝑟) = · ) |
10 | 5, 9 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → 𝑡 = · ) |
11 | 10 | oveqd 6566 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → (𝑎𝑡𝑏) = (𝑎 · 𝑏)) |
12 | 11 | breq2d 4595 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → ( 0 𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎 · 𝑏))) |
13 | 12 | imbi2d 329 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → ((( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)))) |
14 | 13 | 2ralbidv 2972 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)))) |
15 | 14 | sbcbidv 3457 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑡 = (.r‘𝑟)) → ([(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)))) |
16 | 4, 15 | sbcied 3439 |
. . . 4
⊢ (𝑟 = 𝑅 → ([(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)))) |
17 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑟)
∈ V |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V) |
19 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟)) |
20 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
21 | | isorng.0 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑅) |
22 | 20, 21 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = 𝐵) |
24 | 19, 23 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝐵) |
25 | | raleq 3115 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐵 → (∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
26 | 25 | raleqbi1dv 3123 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐵 → (∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
27 | 24, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → (∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
28 | 27 | sbcbidv 3457 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → ([(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
29 | 28 | sbcbidv 3457 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → ([(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
30 | 29 | sbcbidv 3457 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑣 = (Base‘𝑟)) → ([(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
31 | 18, 30 | sbcied 3439 |
. . . . 5
⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
32 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑟) ∈ V |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (0g‘𝑟) ∈ V) |
34 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → 𝑧 = (0g‘𝑟)) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
36 | | isorng.1 |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝑅) |
37 | 35, 36 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → (0g‘𝑟) = 0 ) |
39 | 34, 38 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → 𝑧 = 0 ) |
40 | 39 | breq1d 4593 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → (𝑧𝑙𝑎 ↔ 0 𝑙𝑎)) |
41 | 39 | breq1d 4593 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → (𝑧𝑙𝑏 ↔ 0 𝑙𝑏)) |
42 | 40, 41 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) ↔ ( 0 𝑙𝑎 ∧ 0 𝑙𝑏))) |
43 | 39 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → (𝑧𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎𝑡𝑏))) |
44 | 42, 43 | imbi12d 333 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → (((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)))) |
45 | 44 | 2ralbidv 2972 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)))) |
46 | 45 | sbcbidv 3457 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → ([(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)))) |
47 | 46 | sbcbidv 3457 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑧 = (0g‘𝑟)) → ([(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)))) |
48 | 33, 47 | sbcied 3439 |
. . . . 5
⊢ (𝑟 = 𝑅 → ([(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)))) |
49 | 31, 48 | bitr2d 268 |
. . . 4
⊢ (𝑟 = 𝑅 → ([(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)))) |
50 | | fvex 6113 |
. . . . . 6
⊢
(le‘𝑟) ∈
V |
51 | 50 | a1i 11 |
. . . . 5
⊢ (𝑟 = 𝑅 → (le‘𝑟) ∈ V) |
52 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → 𝑙 = (le‘𝑟)) |
53 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → 𝑟 = 𝑅) |
54 | 53 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → (le‘𝑟) = (le‘𝑅)) |
55 | | isorng.3 |
. . . . . . . . . . 11
⊢ ≤ =
(le‘𝑅) |
56 | 54, 55 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → (le‘𝑟) = ≤ ) |
57 | 52, 56 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → 𝑙 = ≤ ) |
58 | 57 | breqd 4594 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → ( 0 𝑙𝑎 ↔ 0 ≤ 𝑎)) |
59 | 57 | breqd 4594 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → ( 0 𝑙𝑏 ↔ 0 ≤ 𝑏)) |
60 | 58, 59 | anbi12d 743 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) ↔ ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏))) |
61 | 57 | breqd 4594 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → ( 0 𝑙(𝑎 · 𝑏) ↔ 0 ≤ (𝑎 · 𝑏))) |
62 | 60, 61 | imbi12d 333 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → ((( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
63 | 62 | 2ralbidv 2972 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑙 = (le‘𝑟)) → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
64 | 51, 63 | sbcied 3439 |
. . . 4
⊢ (𝑟 = 𝑅 → ([(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 𝑙𝑎 ∧ 0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
65 | 16, 49, 64 | 3bitr3d 297 |
. . 3
⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
66 | | df-orng 29128 |
. . 3
⊢ oRing =
{𝑟 ∈ (Ring ∩ oGrp)
∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))} |
67 | 65, 66 | elrab2 3333 |
. 2
⊢ (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
68 | | df-3an 1033 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |
69 | 2, 67, 68 | 3bitr4i 291 |
1
⊢ (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏) → 0 ≤ (𝑎 · 𝑏)))) |