Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. 2
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ Ring) |
2 | | ringgrp 18552 |
. . . 4
⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) |
3 | 2 | adantl 482 |
. . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ Grp) |
4 | | orngogrp 29801 |
. . . . 5
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) |
5 | | isogrp 29702 |
. . . . . 6
⊢ (𝑅 ∈ oGrp ↔ (𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd)) |
6 | 5 | simprbi 480 |
. . . . 5
⊢ (𝑅 ∈ oGrp → 𝑅 ∈ oMnd) |
7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oMnd) |
8 | | ringmnd 18556 |
. . . 4
⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Mnd) |
9 | | submomnd 29710 |
. . . 4
⊢ ((𝑅 ∈ oMnd ∧ (𝑅 ↾s 𝐴) ∈ Mnd) → (𝑅 ↾s 𝐴) ∈ oMnd) |
10 | 7, 8, 9 | syl2an 494 |
. . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oMnd) |
11 | | isogrp 29702 |
. . 3
⊢ ((𝑅 ↾s 𝐴) ∈ oGrp ↔ ((𝑅 ↾s 𝐴) ∈ Grp ∧ (𝑅 ↾s 𝐴) ∈ oMnd)) |
12 | 3, 10, 11 | sylanbrc 698 |
. 2
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oGrp) |
13 | | simp-4l 806 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑅 ∈ oRing) |
14 | | reldmress 15926 |
. . . . . . . . . . . . . . 15
⊢ Rel dom
↾s |
15 | 14 | ovprc2 6685 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ V → (𝑅 ↾s 𝐴) = ∅) |
16 | 15 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (¬
𝐴 ∈ V →
(Base‘(𝑅
↾s 𝐴)) =
(Base‘∅)) |
17 | 16 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑅
↾s 𝐴)) =
(Base‘∅)) |
18 | | base0 15912 |
. . . . . . . . . . . 12
⊢ ∅ =
(Base‘∅) |
19 | 17, 18 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑅
↾s 𝐴)) =
∅) |
20 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(𝑅
↾s 𝐴)) =
(Base‘(𝑅
↾s 𝐴)) |
21 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(1r‘(𝑅 ↾s 𝐴)) = (1r‘(𝑅 ↾s 𝐴)) |
22 | 20, 21 | ringidcl 18568 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ↾s 𝐴) ∈ Ring →
(1r‘(𝑅
↾s 𝐴))
∈ (Base‘(𝑅
↾s 𝐴))) |
23 | | ne0i 3921 |
. . . . . . . . . . . . . 14
⊢
((1r‘(𝑅 ↾s 𝐴)) ∈ (Base‘(𝑅 ↾s 𝐴)) → (Base‘(𝑅 ↾s 𝐴)) ≠ ∅) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ↾s 𝐴) ∈ Ring →
(Base‘(𝑅
↾s 𝐴))
≠ ∅) |
25 | 24 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑅
↾s 𝐴))
≠ ∅) |
26 | 25 | neneqd 2799 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ ¬ 𝐴 ∈ V) → ¬
(Base‘(𝑅
↾s 𝐴)) =
∅) |
27 | 19, 26 | condan 835 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → 𝐴 ∈ V) |
28 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) |
29 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
30 | 28, 29 | ressbas 15930 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∩ (Base‘𝑅)) = (Base‘(𝑅 ↾s 𝐴))) |
31 | | inss2 3834 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (Base‘𝑅)) ⊆ (Base‘𝑅) |
32 | 30, 31 | syl6eqssr 3656 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V →
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅)) |
33 | 27, 32 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅)) |
34 | 33 | ad3antrrr 766 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (Base‘(𝑅 ↾s 𝐴)) ⊆ (Base‘𝑅)) |
35 | | simpllr 799 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) |
36 | 34, 35 | sseldd 3604 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑎 ∈ (Base‘𝑅)) |
37 | | simprl 794 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎) |
38 | | orngring 29800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) |
39 | | ringgrp 18552 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Grp) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → 𝑅 ∈ Grp) |
42 | 29 | ressinbas 15936 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ V → (𝑅 ↾s 𝐴) = (𝑅 ↾s (𝐴 ∩ (Base‘𝑅)))) |
43 | 30 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ V → (𝑅 ↾s (𝐴 ∩ (Base‘𝑅))) = (𝑅 ↾s (Base‘(𝑅 ↾s 𝐴)))) |
44 | 42, 43 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ V → (𝑅 ↾s 𝐴) = (𝑅 ↾s (Base‘(𝑅 ↾s 𝐴)))) |
45 | 27, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) = (𝑅 ↾s (Base‘(𝑅 ↾s 𝐴)))) |
46 | 45, 3 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s
(Base‘(𝑅
↾s 𝐴)))
∈ Grp) |
47 | 29 | issubg 17594 |
. . . . . . . . . . . . . 14
⊢
((Base‘(𝑅
↾s 𝐴))
∈ (SubGrp‘𝑅)
↔ (𝑅 ∈ Grp ∧
(Base‘(𝑅
↾s 𝐴))
⊆ (Base‘𝑅)
∧ (𝑅
↾s (Base‘(𝑅 ↾s 𝐴))) ∈ Grp)) |
48 | 41, 33, 46, 47 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(Base‘(𝑅
↾s 𝐴))
∈ (SubGrp‘𝑅)) |
49 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ↾s
(Base‘(𝑅
↾s 𝐴))) =
(𝑅 ↾s
(Base‘(𝑅
↾s 𝐴))) |
50 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑅) = (0g‘𝑅) |
51 | 49, 50 | subg0 17600 |
. . . . . . . . . . . . 13
⊢
((Base‘(𝑅
↾s 𝐴))
∈ (SubGrp‘𝑅)
→ (0g‘𝑅) = (0g‘(𝑅 ↾s (Base‘(𝑅 ↾s 𝐴))))) |
52 | 48, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(0g‘𝑅) =
(0g‘(𝑅
↾s (Base‘(𝑅 ↾s 𝐴))))) |
53 | 45 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(0g‘(𝑅
↾s 𝐴)) =
(0g‘(𝑅
↾s (Base‘(𝑅 ↾s 𝐴))))) |
54 | 52, 53 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
(0g‘𝑅) =
(0g‘(𝑅
↾s 𝐴))) |
55 | 54 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝐴))) |
56 | 27 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → 𝐴 ∈ V) |
57 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(le‘𝑅) =
(le‘𝑅) |
58 | 28, 57 | ressle 16059 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (le‘𝑅) = (le‘(𝑅 ↾s 𝐴))) |
59 | 56, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → (le‘𝑅) = (le‘(𝑅 ↾s 𝐴))) |
60 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → 𝑎 = 𝑎) |
61 | 55, 59, 60 | breq123d 4667 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → ((0g‘𝑅)(le‘𝑅)𝑎 ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎)) |
62 | 61 | adantr 481 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → ((0g‘𝑅)(le‘𝑅)𝑎 ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎)) |
63 | 37, 62 | mpbird 247 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅)(le‘𝑅)𝑎) |
64 | | simplr 792 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) |
65 | 34, 64 | sseldd 3604 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝑏 ∈ (Base‘𝑅)) |
66 | | simprr 796 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) |
67 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → 𝑏 = 𝑏) |
68 | 55, 59, 67 | breq123d 4667 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → ((0g‘𝑅)(le‘𝑅)𝑏 ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) |
69 | 68 | adantr 481 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → ((0g‘𝑅)(le‘𝑅)𝑏 ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) |
70 | 66, 69 | mpbird 247 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅)(le‘𝑅)𝑏) |
71 | | eqid 2622 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
72 | 29, 57, 50, 71 | orngmul 29803 |
. . . . . . 7
⊢ ((𝑅 ∈ oRing ∧ (𝑎 ∈ (Base‘𝑅) ∧
(0g‘𝑅)(le‘𝑅)𝑎) ∧ (𝑏 ∈ (Base‘𝑅) ∧ (0g‘𝑅)(le‘𝑅)𝑏)) → (0g‘𝑅)(le‘𝑅)(𝑎(.r‘𝑅)𝑏)) |
73 | 13, 36, 63, 65, 70, 72 | syl122anc 1335 |
. . . . . 6
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅)(le‘𝑅)(𝑎(.r‘𝑅)𝑏)) |
74 | 55 | adantr 481 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝐴))) |
75 | 59 | adantr 481 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (le‘𝑅) = (le‘(𝑅 ↾s 𝐴))) |
76 | 56 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → 𝐴 ∈ V) |
77 | 28, 71 | ressmulr 16006 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(.r‘𝑅) =
(.r‘(𝑅
↾s 𝐴))) |
78 | 76, 77 | syl 17 |
. . . . . . . 8
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (.r‘𝑅) = (.r‘(𝑅 ↾s 𝐴))) |
79 | 78 | oveqd 6667 |
. . . . . . 7
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (𝑎(.r‘𝑅)𝑏) = (𝑎(.r‘(𝑅 ↾s 𝐴))𝑏)) |
80 | 74, 75, 79 | breq123d 4667 |
. . . . . 6
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → ((0g‘𝑅)(le‘𝑅)(𝑎(.r‘𝑅)𝑏) ↔ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) |
81 | 73, 80 | mpbid 222 |
. . . . 5
⊢
(((((𝑅 ∈ oRing
∧ (𝑅
↾s 𝐴)
∈ Ring) ∧ 𝑎 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ 𝑏 ∈
(Base‘(𝑅
↾s 𝐴)))
∧ ((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏)) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏)) |
82 | 81 | ex 450 |
. . . 4
⊢ ((((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ 𝑎 ∈ (Base‘(𝑅 ↾s 𝐴))) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))) → (((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) |
83 | 82 | anasss 679 |
. . 3
⊢ (((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝑎 ∈ (Base‘(𝑅 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝐴)))) → (((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) |
84 | 83 | ralrimivva 2971 |
. 2
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) →
∀𝑎 ∈
(Base‘(𝑅
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))(((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏))) |
85 | | eqid 2622 |
. . 3
⊢
(0g‘(𝑅 ↾s 𝐴)) = (0g‘(𝑅 ↾s 𝐴)) |
86 | | eqid 2622 |
. . 3
⊢
(.r‘(𝑅 ↾s 𝐴)) = (.r‘(𝑅 ↾s 𝐴)) |
87 | | eqid 2622 |
. . 3
⊢
(le‘(𝑅
↾s 𝐴)) =
(le‘(𝑅
↾s 𝐴)) |
88 | 20, 85, 86, 87 | isorng 29799 |
. 2
⊢ ((𝑅 ↾s 𝐴) ∈ oRing ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ oGrp ∧
∀𝑎 ∈
(Base‘(𝑅
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑅 ↾s 𝐴))(((0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑎 ∧ (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))𝑏) → (0g‘(𝑅 ↾s 𝐴))(le‘(𝑅 ↾s 𝐴))(𝑎(.r‘(𝑅 ↾s 𝐴))𝑏)))) |
89 | 1, 12, 84, 88 | syl3anbrc 1246 |
1
⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing) |