Step | Hyp | Ref
| Expression |
1 | | mndmgm 17123 |
. . . . 5
⊢ (𝑆 ∈ Mnd → 𝑆 ∈ Mgm) |
2 | 1 | anim1i 590 |
. . . 4
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm)) |
3 | 2 | 3adant3 1074 |
. . 3
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (#‘𝐵) = 1) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm)) |
4 | 3 | ancomd 466 |
. 2
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (#‘𝐵) = 1) → (𝑇 ∈ Mgm ∧ 𝑆 ∈ Mgm)) |
5 | | zrrhm.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑇) |
6 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑇)
∈ V |
7 | 5, 6 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
8 | | hash1snb 13068 |
. . . . 5
⊢ (𝐵 ∈ V → ((#‘𝐵) = 1 ↔ ∃𝑏 𝐵 = {𝑏})) |
9 | 7, 8 | ax-mp 5 |
. . . 4
⊢
((#‘𝐵) = 1
↔ ∃𝑏 𝐵 = {𝑏}) |
10 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | | zrrhm.0 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑆) |
12 | 10, 11 | mndidcl 17131 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Mnd → 0 ∈
(Base‘𝑆)) |
13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) → 0 ∈
(Base‘𝑆)) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → 0 ∈ (Base‘𝑆)) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑥 ∈ 𝐵) → 0 ∈ (Base‘𝑆)) |
16 | | zrrhm.h |
. . . . . . . 8
⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) |
17 | 15, 16 | fmptd 6292 |
. . . . . . 7
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → 𝐻:𝐵⟶(Base‘𝑆)) |
18 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )) |
19 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑥 = 𝑏) → 0 = 0 ) |
20 | | vsnid 4156 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ {𝑏} |
21 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐵 = {𝑏} → 𝑏 ∈ {𝑏}) |
22 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝐵 = {𝑏} → (𝑏 ∈ 𝐵 ↔ 𝑏 ∈ {𝑏})) |
23 | 21, 22 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝐵 = {𝑏} → 𝑏 ∈ 𝐵) |
24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → 𝑏 ∈ 𝐵) |
25 | 18, 19, 24, 14 | fvmptd 6197 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (𝐻‘𝑏) = 0 ) |
26 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ (𝐻‘𝑏) = 0 ) → (𝐻‘𝑏) = 0 ) |
27 | 26, 26 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ (𝐻‘𝑏) = 0 ) → ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏)) = ( 0 (+g‘𝑆) 0 )) |
28 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝑆) = (+g‘𝑆) |
29 | 10, 28, 11 | mndlid 17134 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Mnd ∧ 0 ∈
(Base‘𝑆)) → (
0
(+g‘𝑆)
0 ) =
0
) |
30 | 12, 29 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Mnd → ( 0
(+g‘𝑆)
0 ) =
0
) |
31 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) → ( 0
(+g‘𝑆)
0 ) =
0
) |
32 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → ( 0 (+g‘𝑆) 0 ) = 0 ) |
33 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ (𝐻‘𝑏) = 0 ) → ( 0
(+g‘𝑆)
0 ) =
0
) |
34 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) → 𝑇 ∈ Mgm) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → 𝑇 ∈ Mgm) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑏 ∈ 𝐵) → 𝑇 ∈ Mgm) |
37 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
38 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝑇) = (+g‘𝑇) |
39 | 5, 38 | mgmcl 17068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ Mgm ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑏(+g‘𝑇)𝑏) ∈ 𝐵) |
40 | 36, 37, 37, 39 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑏 ∈ 𝐵) → (𝑏(+g‘𝑇)𝑏) ∈ 𝐵) |
41 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = {𝑏} → ((𝑏(+g‘𝑇)𝑏) ∈ 𝐵 ↔ (𝑏(+g‘𝑇)𝑏) ∈ {𝑏})) |
42 | | elsni 4142 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏(+g‘𝑇)𝑏) ∈ {𝑏} → (𝑏(+g‘𝑇)𝑏) = 𝑏) |
43 | 41, 42 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = {𝑏} → ((𝑏(+g‘𝑇)𝑏) ∈ 𝐵 → (𝑏(+g‘𝑇)𝑏) = 𝑏)) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → ((𝑏(+g‘𝑇)𝑏) ∈ 𝐵 → (𝑏(+g‘𝑇)𝑏) = 𝑏)) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑏 ∈ 𝐵) → ((𝑏(+g‘𝑇)𝑏) ∈ 𝐵 → (𝑏(+g‘𝑇)𝑏) = 𝑏)) |
46 | 40, 45 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ 𝑏 ∈ 𝐵) → (𝑏(+g‘𝑇)𝑏) = 𝑏) |
47 | 24, 46 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (𝑏(+g‘𝑇)𝑏) = 𝑏) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (𝐻‘(𝑏(+g‘𝑇)𝑏)) = (𝐻‘𝑏)) |
49 | 48 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ (𝐻‘𝑏) = 0 ) → (𝐻‘(𝑏(+g‘𝑇)𝑏)) = (𝐻‘𝑏)) |
50 | 49, 26 | eqtr2d 2645 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ (𝐻‘𝑏) = 0 ) → 0 = (𝐻‘(𝑏(+g‘𝑇)𝑏))) |
51 | 27, 33, 50 | 3eqtrrd 2649 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) ∧ (𝐻‘𝑏) = 0 ) → (𝐻‘(𝑏(+g‘𝑇)𝑏)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏))) |
52 | 25, 51 | mpdan 699 |
. . . . . . . 8
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (𝐻‘(𝑏(+g‘𝑇)𝑏)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏))) |
53 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐵 = {𝑏} → 𝐵 = {𝑏}) |
54 | 53 | raleqdv 3121 |
. . . . . . . . . . 11
⊢ (𝐵 = {𝑏} → (∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑐 ∈ {𝑏} (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)))) |
55 | 53, 54 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (𝐵 = {𝑏} → (∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑎 ∈ {𝑏}∀𝑐 ∈ {𝑏} (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)))) |
56 | 55 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ ∀𝑎 ∈ {𝑏}∀𝑐 ∈ {𝑏} (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)))) |
57 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
58 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝑎(+g‘𝑇)𝑐) = (𝑏(+g‘𝑇)𝑐)) |
59 | 58 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝐻‘(𝑎(+g‘𝑇)𝑐)) = (𝐻‘(𝑏(+g‘𝑇)𝑐))) |
60 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝐻‘𝑎) = (𝐻‘𝑏)) |
61 | 60 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑐))) |
62 | 59, 61 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → ((𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘(𝑏(+g‘𝑇)𝑐)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑐)))) |
63 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑏 → (𝑏(+g‘𝑇)𝑐) = (𝑏(+g‘𝑇)𝑏)) |
64 | 63 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑏 → (𝐻‘(𝑏(+g‘𝑇)𝑐)) = (𝐻‘(𝑏(+g‘𝑇)𝑏))) |
65 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑏 → (𝐻‘𝑐) = (𝐻‘𝑏)) |
66 | 65 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑏 → ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑐)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏))) |
67 | 64, 66 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑏 → ((𝐻‘(𝑏(+g‘𝑇)𝑐)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘(𝑏(+g‘𝑇)𝑏)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏)))) |
68 | 62, 67 | 2ralsng 4167 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ V ∧ 𝑏 ∈ V) → (∀𝑎 ∈ {𝑏}∀𝑐 ∈ {𝑏} (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘(𝑏(+g‘𝑇)𝑏)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏)))) |
69 | 57, 57, 68 | mp2an 704 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
{𝑏}∀𝑐 ∈ {𝑏} (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘(𝑏(+g‘𝑇)𝑏)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏))) |
70 | 56, 69 | syl6bb 275 |
. . . . . . . 8
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)) ↔ (𝐻‘(𝑏(+g‘𝑇)𝑏)) = ((𝐻‘𝑏)(+g‘𝑆)(𝐻‘𝑏)))) |
71 | 52, 70 | mpbird 246 |
. . . . . . 7
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐))) |
72 | 17, 71 | jca 553 |
. . . . . 6
⊢ (((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) ∧ 𝐵 = {𝑏}) → (𝐻:𝐵⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)))) |
73 | 72 | ex 449 |
. . . . 5
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) → (𝐵 = {𝑏} → (𝐻:𝐵⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐))))) |
74 | 73 | exlimdv 1848 |
. . . 4
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) →
(∃𝑏 𝐵 = {𝑏} → (𝐻:𝐵⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐))))) |
75 | 9, 74 | syl5bi 231 |
. . 3
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm) →
((#‘𝐵) = 1 →
(𝐻:𝐵⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐))))) |
76 | 75 | 3impia 1253 |
. 2
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (#‘𝐵) = 1) → (𝐻:𝐵⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐)))) |
77 | 5, 10, 38, 28 | ismgmhm 41573 |
. 2
⊢ (𝐻 ∈ (𝑇 MgmHom 𝑆) ↔ ((𝑇 ∈ Mgm ∧ 𝑆 ∈ Mgm) ∧ (𝐻:𝐵⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑇)𝑐)) = ((𝐻‘𝑎)(+g‘𝑆)(𝐻‘𝑐))))) |
78 | 4, 76, 77 | sylanbrc 695 |
1
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ (#‘𝐵) = 1) → 𝐻 ∈ (𝑇 MgmHom 𝑆)) |