Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝑅 ∈ Ring) |
2 | | lidlabl.l |
. . . . . . . 8
⊢ 𝐿 = (LIdeal‘𝑅) |
3 | | zlidlring.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑅) |
4 | 2, 3 | lidl0 19219 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → { 0 } ∈
𝐿) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → { 0 } ∈
𝐿) |
6 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑈 = { 0 } → (𝑈 ∈ 𝐿 ↔ { 0 } ∈ 𝐿)) |
7 | 6 | adantl 482 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝑈 ∈ 𝐿 ↔ { 0 } ∈ 𝐿)) |
8 | 5, 7 | mpbird 247 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝑈 ∈ 𝐿) |
9 | 1, 8 | jca 554 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿)) |
10 | | lidlabl.i |
. . . . 5
⊢ 𝐼 = (𝑅 ↾s 𝑈) |
11 | 2, 10 | lidlrng 41927 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿) → 𝐼 ∈ Rng) |
12 | 9, 11 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Rng) |
13 | | eleq1 2689 |
. . . . . . 7
⊢ ({ 0 } = 𝑈 → ({ 0 } ∈ 𝐿 ↔ 𝑈 ∈ 𝐿)) |
14 | 13 | eqcoms 2630 |
. . . . . 6
⊢ (𝑈 = { 0 } → ({ 0 } ∈
𝐿 ↔ 𝑈 ∈ 𝐿)) |
15 | 14 | adantl 482 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ({ 0 } ∈
𝐿 ↔ 𝑈 ∈ 𝐿)) |
16 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
17 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) |
18 | 17, 3 | ring0cl 18569 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 0 ∈
(Base‘𝑅)) |
19 | 16, 18 | jca 554 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → (𝑅 ∈ Ring ∧ 0 ∈
(Base‘𝑅))) |
20 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
21 | 17, 20, 3 | ringlz 18587 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 0 ∈
(Base‘𝑅)) → (
0
(.r‘𝑅)
0 ) =
0
) |
22 | 21, 21 | jca 554 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 0 ∈
(Base‘𝑅)) → ((
0
(.r‘𝑅)
0 ) =
0 ∧ (
0
(.r‘𝑅)
0 ) =
0
)) |
23 | 19, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → (( 0
(.r‘𝑅)
0 ) =
0 ∧ (
0
(.r‘𝑅)
0 ) =
0
)) |
24 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑅) ∈ V |
25 | 3, 24 | eqeltri 2697 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
26 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 0 ∈
V) |
27 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → ( 0
(.r‘𝑅)𝑦) = ( 0 (.r‘𝑅) 0 )) |
28 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → 𝑦 = 0 ) |
29 | 27, 28 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (( 0
(.r‘𝑅)𝑦) = 𝑦 ↔ ( 0 (.r‘𝑅) 0 ) = 0 )) |
30 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (𝑦(.r‘𝑅) 0 ) = ( 0 (.r‘𝑅) 0 )) |
31 | 30, 28 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → ((𝑦(.r‘𝑅) 0 ) = 𝑦 ↔ ( 0 (.r‘𝑅) 0 ) = 0 )) |
32 | 29, 31 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → ((( 0
(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦) ↔ (( 0 (.r‘𝑅) 0 ) = 0 ∧ ( 0 (.r‘𝑅) 0 ) = 0 ))) |
33 | 32 | ralsng 4218 |
. . . . . . . . . . . 12
⊢ ( 0 ∈ V
→ (∀𝑦 ∈ {
0 } ((
0
(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦) ↔ (( 0 (.r‘𝑅) 0 ) = 0 ∧ ( 0 (.r‘𝑅) 0 ) = 0 ))) |
34 | 26, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(∀𝑦 ∈ { 0 } (( 0
(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦) ↔ (( 0 (.r‘𝑅) 0 ) = 0 ∧ ( 0 (.r‘𝑅) 0 ) = 0 ))) |
35 | 23, 34 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
∀𝑦 ∈ { 0 } (( 0
(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦)) |
36 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝑥(.r‘𝑅)𝑦) = ( 0 (.r‘𝑅)𝑦)) |
37 | 36 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → ((𝑥(.r‘𝑅)𝑦) = 𝑦 ↔ ( 0 (.r‘𝑅)𝑦) = 𝑦)) |
38 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝑦(.r‘𝑅)𝑥) = (𝑦(.r‘𝑅) 0 )) |
39 | 38 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → ((𝑦(.r‘𝑅)𝑥) = 𝑦 ↔ (𝑦(.r‘𝑅) 0 ) = 𝑦)) |
40 | 37, 39 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦) ↔ (( 0 (.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦))) |
41 | 40 | ralbidv 2986 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } (( 0 (.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦))) |
42 | 41 | rexsng 4219 |
. . . . . . . . . . 11
⊢ ( 0 ∈ V
→ (∃𝑥 ∈ {
0
}∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } (( 0 (.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦))) |
43 | 26, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(∃𝑥 ∈ { 0
}∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } (( 0 (.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅) 0 ) = 𝑦))) |
44 | 35, 43 | mpbird 247 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)) |
45 | 44 | adantr 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)) |
46 | 45 | adantr 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)) |
47 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → 𝑈 ∈ 𝐿) |
48 | 2, 10 | lidlbas 41923 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝐿 → (Base‘𝐼) = 𝑈) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (Base‘𝐼) = 𝑈) |
50 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝑈 = { 0 }) |
51 | 50 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → 𝑈 = { 0 }) |
52 | 49, 51 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (Base‘𝐼) = { 0 }) |
53 | 10, 20 | ressmulr 16006 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ 𝐿 → (.r‘𝑅) = (.r‘𝐼)) |
54 | 53 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ 𝐿 → (.r‘𝐼) = (.r‘𝑅)) |
55 | 54 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (.r‘𝐼) = (.r‘𝑅)) |
56 | 55 | oveqd 6667 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (𝑥(.r‘𝐼)𝑦) = (𝑥(.r‘𝑅)𝑦)) |
57 | 56 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → ((𝑥(.r‘𝐼)𝑦) = 𝑦 ↔ (𝑥(.r‘𝑅)𝑦) = 𝑦)) |
58 | 55 | oveqd 6667 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (𝑦(.r‘𝐼)𝑥) = (𝑦(.r‘𝑅)𝑥)) |
59 | 58 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → ((𝑦(.r‘𝐼)𝑥) = 𝑦 ↔ (𝑦(.r‘𝑅)𝑥) = 𝑦)) |
60 | 57, 59 | anbi12d 747 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦) ↔ ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
61 | 52, 60 | raleqbidv 3152 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦) ↔ ∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
62 | 52, 61 | rexeqbidv 3153 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → (∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦) ↔ ∃𝑥 ∈ { 0 }∀𝑦 ∈ { 0 } ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
63 | 46, 62 | mpbird 247 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) ∧ 𝑈 ∈ 𝐿) → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦)) |
64 | 63 | ex 450 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝑈 ∈ 𝐿 → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦))) |
65 | 15, 64 | sylbid 230 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ({ 0 } ∈
𝐿 → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦))) |
66 | 5, 65 | mpd 15 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦)) |
67 | 12, 66 | jca 554 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → (𝐼 ∈ Rng ∧ ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦))) |
68 | | eqid 2622 |
. . 3
⊢
(Base‘𝐼) =
(Base‘𝐼) |
69 | | eqid 2622 |
. . 3
⊢
(.r‘𝐼) = (.r‘𝐼) |
70 | 68, 69 | isringrng 41881 |
. 2
⊢ (𝐼 ∈ Ring ↔ (𝐼 ∈ Rng ∧ ∃𝑥 ∈ (Base‘𝐼)∀𝑦 ∈ (Base‘𝐼)((𝑥(.r‘𝐼)𝑦) = 𝑦 ∧ (𝑦(.r‘𝐼)𝑥) = 𝑦))) |
71 | 67, 70 | sylibr 224 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑈 = { 0 }) → 𝐼 ∈ Ring) |