Step | Hyp | Ref
| Expression |
1 | | mndmgm 18213 |
. . 3
⊢ (𝑇 ∈ Mnd → 𝑇 ∈ Mgm) |
2 | 1 | anim2i 620 |
. 2
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm)) |
3 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝑇) =
(Base‘𝑇) |
4 | | c0mhm.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑇) |
5 | 3, 4 | mndidcl 18221 |
. . . . . 6
⊢ (𝑇 ∈ Mnd → 0 ∈
(Base‘𝑇)) |
6 | 5 | adantl 485 |
. . . . 5
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 0 ∈
(Base‘𝑇)) |
7 | 6 | adantr 484 |
. . . 4
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ 𝑥 ∈ 𝐵) → 0 ∈ (Base‘𝑇)) |
8 | | c0mhm.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 ) |
9 | 7, 8 | fmptd 6953 |
. . 3
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 𝐻:𝐵⟶(Base‘𝑇)) |
10 | 5 | ancli 552 |
. . . . . . . 8
⊢ (𝑇 ∈ Mnd → (𝑇 ∈ Mnd ∧ 0 ∈
(Base‘𝑇))) |
11 | 10 | adantl 485 |
. . . . . . 7
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → (𝑇 ∈ Mnd ∧ 0 ∈
(Base‘𝑇))) |
12 | | eqid 2739 |
. . . . . . . 8
⊢
(+g‘𝑇) = (+g‘𝑇) |
13 | 3, 12, 4 | mndlid 18226 |
. . . . . . 7
⊢ ((𝑇 ∈ Mnd ∧ 0 ∈
(Base‘𝑇)) → (
0
(+g‘𝑇)
0 ) =
0
) |
14 | 11, 13 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → ( 0
(+g‘𝑇)
0 ) =
0
) |
15 | 14 | adantr 484 |
. . . . 5
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( 0 (+g‘𝑇) 0 ) = 0 ) |
16 | 8 | a1i 11 |
. . . . . . 7
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐻 = (𝑥 ∈ 𝐵 ↦ 0 )) |
17 | | eqidd 2740 |
. . . . . . 7
⊢ ((((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = 𝑎) → 0 = 0 ) |
18 | | simprl 771 |
. . . . . . 7
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
19 | 6 | adantr 484 |
. . . . . . 7
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 0 ∈ (Base‘𝑇)) |
20 | 16, 17, 18, 19 | fvmptd 6847 |
. . . . . 6
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐻‘𝑎) = 0 ) |
21 | | eqidd 2740 |
. . . . . . 7
⊢ ((((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = 𝑏) → 0 = 0 ) |
22 | | simprr 773 |
. . . . . . 7
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
23 | 16, 21, 22, 19 | fvmptd 6847 |
. . . . . 6
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐻‘𝑏) = 0 ) |
24 | 20, 23 | oveq12d 7253 |
. . . . 5
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐻‘𝑎)(+g‘𝑇)(𝐻‘𝑏)) = ( 0 (+g‘𝑇) 0 )) |
25 | | eqidd 2740 |
. . . . . 6
⊢ ((((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑥 = (𝑎(+g‘𝑆)𝑏)) → 0 = 0 ) |
26 | | c0mhm.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
27 | | eqid 2739 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘𝑆) |
28 | 26, 27 | mgmcl 18150 |
. . . . . . . 8
⊢ ((𝑆 ∈ Mgm ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑆)𝑏) ∈ 𝐵) |
29 | 28 | 3expb 1122 |
. . . . . . 7
⊢ ((𝑆 ∈ Mgm ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑆)𝑏) ∈ 𝐵) |
30 | 29 | adantlr 715 |
. . . . . 6
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑆)𝑏) ∈ 𝐵) |
31 | 16, 25, 30, 19 | fvmptd 6847 |
. . . . 5
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐻‘(𝑎(+g‘𝑆)𝑏)) = 0 ) |
32 | 15, 24, 31 | 3eqtr4rd 2790 |
. . . 4
⊢ (((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐻‘(𝑎(+g‘𝑆)𝑏)) = ((𝐻‘𝑎)(+g‘𝑇)(𝐻‘𝑏))) |
33 | 32 | ralrimivva 3115 |
. . 3
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) →
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑆)𝑏)) = ((𝐻‘𝑎)(+g‘𝑇)(𝐻‘𝑏))) |
34 | 9, 33 | jca 515 |
. 2
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → (𝐻:𝐵⟶(Base‘𝑇) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑆)𝑏)) = ((𝐻‘𝑎)(+g‘𝑇)(𝐻‘𝑏)))) |
35 | 26, 3, 27, 12 | ismgmhm 45056 |
. 2
⊢ (𝐻 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐻:𝐵⟶(Base‘𝑇) ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝐻‘(𝑎(+g‘𝑆)𝑏)) = ((𝐻‘𝑎)(+g‘𝑇)(𝐻‘𝑏))))) |
36 | 2, 34, 35 | sylanbrc 586 |
1
⊢ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd) → 𝐻 ∈ (𝑆 MgmHom 𝑇)) |