Step | Hyp | Ref
| Expression |
1 | | eldifi 4027 |
. . . . 5
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝑇 ∈
Ring) |
2 | | ringrng 45019 |
. . . . 5
⊢ (𝑇 ∈ Ring → 𝑇 ∈ Rng) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝑇 ∈
Rng) |
4 | 3 | anim1i 618 |
. . 3
⊢ ((𝑇 ∈ (Ring ∖ NzRing)
∧ 𝑆 ∈ Rng) →
(𝑇 ∈ Rng ∧ 𝑆 ∈ Rng)) |
5 | 4 | ancoms 462 |
. 2
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ (𝑇 ∈ Rng ∧
𝑆 ∈
Rng)) |
6 | | rngabl 45017 |
. . . . . 6
⊢ (𝑆 ∈ Rng → 𝑆 ∈ Abel) |
7 | | ablgrp 19042 |
. . . . . 6
⊢ (𝑆 ∈ Abel → 𝑆 ∈ Grp) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝑆 ∈ Rng → 𝑆 ∈ Grp) |
9 | 8 | adantr 484 |
. . . 4
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝑆 ∈
Grp) |
10 | | ringgrp 19434 |
. . . . . 6
⊢ (𝑇 ∈ Ring → 𝑇 ∈ Grp) |
11 | 1, 10 | syl 17 |
. . . . 5
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝑇 ∈
Grp) |
12 | 11 | adantl 485 |
. . . 4
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝑇 ∈
Grp) |
13 | | zrrhm.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑇) |
14 | | eqid 2739 |
. . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) |
15 | 13, 14 | 0ringbas 45011 |
. . . . 5
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ 𝐵 =
{(0g‘𝑇)}) |
16 | 15 | adantl 485 |
. . . 4
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝐵 =
{(0g‘𝑇)}) |
17 | | zrrhm.0 |
. . . . 5
⊢ 0 =
(0g‘𝑆) |
18 | | zrrhm.h |
. . . . 5
⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) |
19 | 13, 17, 18, 14 | c0snghm 45056 |
. . . 4
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = {(0g‘𝑇)}) → 𝐻 ∈ (𝑇 GrpHom 𝑆)) |
20 | 9, 12, 16, 19 | syl3anc 1372 |
. . 3
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝐻 ∈ (𝑇 GrpHom 𝑆)) |
21 | 18 | a1i 11 |
. . . . . . . 8
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )) |
22 | | eqidd 2740 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ 𝑥 =
(0g‘𝑇))
→ 0
= 0
) |
23 | 13, 14 | ring0cl 19454 |
. . . . . . . . . 10
⊢ (𝑇 ∈ Ring →
(0g‘𝑇)
∈ 𝐵) |
24 | 1, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ (0g‘𝑇) ∈ 𝐵) |
25 | 24 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (0g‘𝑇) ∈ 𝐵) |
26 | 17 | fvexi 6701 |
. . . . . . . . 9
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ 0
∈ V) |
28 | 21, 22, 25, 27 | fvmptd 6795 |
. . . . . . 7
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (𝐻‘(0g‘𝑇)) = 0 ) |
29 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑆) =
(Base‘𝑆) |
30 | 29, 17 | grpidcl 18262 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Grp → 0 ∈
(Base‘𝑆)) |
31 | 8, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Rng → 0 ∈
(Base‘𝑆)) |
32 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑆) = (.r‘𝑆) |
33 | 29, 32, 17 | rnglz 45024 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Rng ∧ 0 ∈
(Base‘𝑆)) → (
0
(.r‘𝑆)
0 ) =
0
) |
34 | 31, 33 | mpdan 687 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Rng → ( 0
(.r‘𝑆)
0 ) =
0
) |
35 | 34 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ ( 0 (.r‘𝑆) 0 ) = 0 ) |
36 | 35 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ( 0 (.r‘𝑆) 0 ) = 0 ) |
37 | 36 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → ( 0
(.r‘𝑆)
0 ) =
0
) |
38 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘(0g‘𝑇)) = 0 ) |
39 | 38, 38 | oveq12d 7201 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))) = ( 0 (.r‘𝑆) 0 )) |
40 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑇) = (.r‘𝑇) |
41 | 13, 40, 14 | ringlz 19472 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Ring ∧
(0g‘𝑇)
∈ 𝐵) →
((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
42 | 1, 23, 41 | syl2anc2 588 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ ((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
43 | 42 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
44 | 43 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) →
((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)) = (0g‘𝑇)) |
45 | 44 | fveq2d 6691 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = (𝐻‘(0g‘𝑇))) |
46 | 45, 38 | eqtrd 2774 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = 0 ) |
47 | 37, 39, 46 | 3eqtr4rd 2785 |
. . . . . . 7
⊢ ((((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
∧ (𝐻‘(0g‘𝑇)) = 0 ) → (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇)))) |
48 | 28, 47 | mpdan 687 |
. . . . . 6
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇)))) |
49 | 23, 23 | jca 515 |
. . . . . . . . 9
⊢ (𝑇 ∈ Ring →
((0g‘𝑇)
∈ 𝐵 ∧
(0g‘𝑇)
∈ 𝐵)) |
50 | 1, 49 | syl 17 |
. . . . . . . 8
⊢ (𝑇 ∈ (Ring ∖ NzRing)
→ ((0g‘𝑇) ∈ 𝐵 ∧ (0g‘𝑇) ∈ 𝐵)) |
51 | 50 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ((0g‘𝑇) ∈ 𝐵 ∧ (0g‘𝑇) ∈ 𝐵)) |
52 | | fvoveq1 7206 |
. . . . . . . . 9
⊢ (𝑎 = (0g‘𝑇) → (𝐻‘(𝑎(.r‘𝑇)𝑐)) = (𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐))) |
53 | | fveq2 6687 |
. . . . . . . . . 10
⊢ (𝑎 = (0g‘𝑇) → (𝐻‘𝑎) = (𝐻‘(0g‘𝑇))) |
54 | 53 | oveq1d 7198 |
. . . . . . . . 9
⊢ (𝑎 = (0g‘𝑇) → ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐))) |
55 | 52, 54 | eqeq12d 2755 |
. . . . . . . 8
⊢ (𝑎 = (0g‘𝑇) → ((𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐)))) |
56 | | oveq2 7191 |
. . . . . . . . . 10
⊢ (𝑐 = (0g‘𝑇) →
((0g‘𝑇)(.r‘𝑇)𝑐) = ((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) |
57 | 56 | fveq2d 6691 |
. . . . . . . . 9
⊢ (𝑐 = (0g‘𝑇) → (𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐)) = (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇)))) |
58 | | fveq2 6687 |
. . . . . . . . . 10
⊢ (𝑐 = (0g‘𝑇) → (𝐻‘𝑐) = (𝐻‘(0g‘𝑇))) |
59 | 58 | oveq2d 7199 |
. . . . . . . . 9
⊢ (𝑐 = (0g‘𝑇) → ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇)))) |
60 | 57, 59 | eqeq12d 2755 |
. . . . . . . 8
⊢ (𝑐 = (0g‘𝑇) → ((𝐻‘((0g‘𝑇)(.r‘𝑇)𝑐)) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))))) |
61 | 55, 60 | 2ralsng 4577 |
. . . . . . 7
⊢
(((0g‘𝑇) ∈ 𝐵 ∧ (0g‘𝑇) ∈ 𝐵) → (∀𝑎 ∈ {(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))))) |
62 | 51, 61 | syl 17 |
. . . . . 6
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (∀𝑎 ∈
{(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘((0g‘𝑇)(.r‘𝑇)(0g‘𝑇))) = ((𝐻‘(0g‘𝑇))(.r‘𝑆)(𝐻‘(0g‘𝑇))))) |
63 | 48, 62 | mpbird 260 |
. . . . 5
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ∀𝑎 ∈
{(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))) |
64 | | raleq 3311 |
. . . . . . 7
⊢ (𝐵 = {(0g‘𝑇)} → (∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
65 | 64 | raleqbi1dv 3309 |
. . . . . 6
⊢ (𝐵 = {(0g‘𝑇)} → (∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑎 ∈ {(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
66 | 65 | adantl 485 |
. . . . 5
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ (∀𝑎 ∈
𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑎 ∈ {(0g‘𝑇)}∀𝑐 ∈ {(0g‘𝑇)} (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
67 | 63, 66 | mpbird 260 |
. . . 4
⊢ (((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
∧ 𝐵 =
{(0g‘𝑇)})
→ ∀𝑎 ∈
𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))) |
68 | 16, 67 | mpdan 687 |
. . 3
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ ∀𝑎 ∈
𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))) |
69 | 20, 68 | jca 515 |
. 2
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ (𝐻 ∈ (𝑇 GrpHom 𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐)))) |
70 | 13, 40, 32 | isrnghm 45032 |
. 2
⊢ (𝐻 ∈ (𝑇 RngHomo 𝑆) ↔ ((𝑇 ∈ Rng ∧ 𝑆 ∈ Rng) ∧ (𝐻 ∈ (𝑇 GrpHom 𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(.r‘𝑇)𝑐)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑐))))) |
71 | 5, 69, 70 | sylanbrc 586 |
1
⊢ ((𝑆 ∈ Rng ∧ 𝑇 ∈ (Ring ∖ NzRing))
→ 𝐻 ∈ (𝑇 RngHomo 𝑆)) |