Step | Hyp | Ref
| Expression |
1 | | eldifi 3732 |
. . . . 5
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝑇 ∈
Ring) |
2 | | ringrng 41879 |
. . . . 5
⊢ (𝑇 ∈ Ring → 𝑇 ∈ Rng) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝑇 ∈
Rng) |
4 | 3 | anim1i 592 |
. . 3
⊢ ((𝑇 ∈ (Ring ∖ NzRing)
∧ 𝑆 ∈ Rng) →
(𝑇 ∈ Rng ∧ 𝑆 ∈ Rng)) |
5 | 4 | ancoms 469 |
. 2
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ (𝑇 ∈ Rng ∧
𝑆 ∈
Rng)) |
6 | | rngabl 41877 |
. . . . . 6
⊢ (𝑆 ∈ Rng → 𝑆 ∈ Abel) |
7 | | ablgrp 18198 |
. . . . . 6
⊢ (𝑆 ∈ Abel → 𝑆 ∈ Grp) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝑆 ∈ Rng → 𝑆 ∈ Grp) |
9 | 8 | adantr 481 |
. . . 4
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝑆 ∈
Grp) |
10 | | ringgrp 18552 |
. . . . . 6
⊢ (𝑇 ∈ Ring → 𝑇 ∈ Grp) |
11 | 1, 10 | syl 17 |
. . . . 5
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝑇 ∈
Grp) |
12 | 11 | adantl 482 |
. . . 4
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝑇 ∈
Grp) |
13 | | zrrhm.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑇) |
14 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) |
15 | 13, 14 | 0ringbas 41871 |
. . . . 5
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝐵 =
{(0g‘𝑇)}) |
16 | 15 | adantl 482 |
. . . 4
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝐵 =
{(0g‘𝑇)}) |
17 | | zrrhm.0 |
. . . . 5
⊢ 0 =
(0g‘𝑆) |
18 | | zrrhm.h |
. . . . 5
⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) |
19 | 13, 17, 18, 14 | c0snghm 41916 |
. . . 4
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = {(0g‘𝑇)}) → 𝐻 ∈ (𝑇 GrpHom 𝑆)) |
20 | 9, 12, 16, 19 | syl3anc 1326 |
. . 3
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝐻 ∈ (𝑇 GrpHom 𝑆)) |
21 | 18 | a1i 11 |
. . . . . . . 8
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )) |
22 | | eqidd 2623 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ 𝑥 =
(0g‘𝑇))
→ 0
= 0
) |
23 | 13, 14 | ring0cl 18569 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Ring →
(0g‘𝑇)
∈ 𝐵) |
24 | 1, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ (0g‘𝑇) ∈ 𝐵) |
25 | 24 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (0g‘𝑇) ∈ 𝐵) |
26 | | fvex 6201 |
. . . . . . . . . 10
⊢
(0g‘𝑆) ∈ V |
27 | 17, 26 | eqeltri 2697 |
. . . . . . . . 9
⊢ 0 ∈
V |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ 0
∈ V) |
29 | 21, 22, 25, 28 | fvmptd 6288 |
. . . . . . 7
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (𝐻‘(0g‘𝑇)) = 0 ) |
30 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑆) =
(Base‘𝑆) |
31 | 30, 17 | grpidcl 17450 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Grp → 0 ∈
(Base‘𝑆)) |
32 | 8, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Rng → 0 ∈
(Base‘𝑆)) |
33 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑆) = (.r‘𝑆) |
34 | 30, 33, 17 | rnglz 41884 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Rng ∧ 0 ∈
(Base‘𝑆)) → (
0
(.r‘𝑆)
0 ) =
0
) |
35 | 32, 34 | mpdan 702 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Rng → ( 0
(.r‘𝑆)
0 ) =
0
) |
36 | 35 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ ( 0 (.r‘𝑆) 0 ) = 0 ) |
37 | 36 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ( 0 (.r‘𝑆) 0 ) = 0 ) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → ( 0
(.r‘𝑆)
0 ) =
0
) |
39 | | simpr 477 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘(0g‘𝑇)) = 0 ) |
40 | 39, 39 | oveq12d 6668 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))) = ( 0 (.r‘𝑆) 0 )) |
41 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑇) = (.r‘𝑇) |
42 | 13, 41, 14 | ringlz 18587 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ Ring ∧
(0g‘𝑇)
∈ 𝐵) →
((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
43 | 23, 42 | mpdan 702 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Ring →
((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
44 | 1, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ ((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
45 | 44 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
46 | 45 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) →
((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
47 | 46 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = (𝐻‘(0g‘𝑇))) |
48 | 47, 39 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = 0 ) |
49 | 38, 40, 48 | 3eqtr4rd 2667 |
. . . . . . 7
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇)))) |
50 | 29, 49 | mpdan 702 |
. . . . . 6
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇)))) |
51 | 23, 23 | jca 554 |
. . . . . . . . 9
⊢ (𝑇 ∈ Ring →
((0g‘𝑇)
∈ 𝐵 ∧
(0g‘𝑇)
∈ 𝐵)) |
52 | 1, 51 | syl 17 |
. . . . . . . 8
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ ((0g‘𝑇) ∈ 𝐵 ∧ (0g‘𝑇) ∈ 𝐵)) |
53 | 52 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ((0g‘𝑇) ∈ 𝐵 ∧ (0g‘𝑇) ∈ 𝐵)) |
54 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑎 = (0g‘𝑇) → (𝑎(.r‘𝑇)𝑐) = ((0g‘𝑇)(.r‘𝑇)𝑐)) |
55 | 54 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑎 = (0g‘𝑇) → (𝐻‘(𝑎(.r‘𝑇)𝑐)) = (𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐))) |
56 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑎 = (0g‘𝑇) → (𝐻‘𝑎) = (𝐻‘(0g‘𝑇))) |
57 | 56 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑎 = (0g‘𝑇) → ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐))) |
58 | 55, 57 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑎 = (0g‘𝑇) → ((𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐)))) |
59 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑐 = (0g‘𝑇) →
((0g‘𝑇)(.r‘𝑇)𝑐) = ((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) |
60 | 59 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑐 = (0g‘𝑇) → (𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐)) = (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)))) |
61 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑐 = (0g‘𝑇) → (𝐻‘𝑐) = (𝐻‘(0g‘𝑇))) |
62 | 61 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑐 = (0g‘𝑇) → ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇)))) |
63 | 60, 62 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑐 = (0g‘𝑇) → ((𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))))) |
64 | 58, 63 | 2ralsng 4220 |
. . . . . . 7
⊢
(((0g‘𝑇) ∈ 𝐵 ∧ (0g‘𝑇) ∈ 𝐵) → (∀𝑎 ∈ {(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))))) |
65 | 53, 64 | syl 17 |
. . . . . 6
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (∀𝑎 ∈
{(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))))) |
66 | 50, 65 | mpbird 247 |
. . . . 5
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ∀𝑎 ∈
{(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))) |
67 | | raleq 3138 |
. . . . . . 7
⊢ (𝐵 = {(0g‘𝑇)} → (∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
68 | 67 | raleqbi1dv 3146 |
. . . . . 6
⊢ (𝐵 = {(0g‘𝑇)} → (∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑎 ∈ {(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
69 | 68 | adantl 482 |
. . . . 5
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (∀𝑎 ∈
𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑎 ∈ {(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
70 | 66, 69 | mpbird 247 |
. . . 4
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ∀𝑎 ∈
𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))) |
71 | 16, 70 | mpdan 702 |
. . 3
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ ∀𝑎 ∈
𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))) |
72 | 20, 71 | jca 554 |
. 2
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ (𝐻 ∈ (𝑇 GrpHom 𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
73 | 13, 41, 33 | isrnghm 41892 |
. 2
⊢ (𝐻 ∈ (𝑇 RngHomo 𝑆) ↔ ((𝑇 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐻 ∈ (𝑇 GrpHom 𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))))) |
74 | 5, 72, 73 | sylanbrc 698 |
1
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝐻 ∈ (𝑇 RngHomo 𝑆)) |