Step | Hyp | Ref
| Expression |
1 | | mgmhmrcl 42309 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm)) |
2 | 1 | simpld 477 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝑆 ∈ Mgm) |
3 | 2 | adantl 473 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝑆 ∈ Mgm) |
4 | | resmgmhm2.u |
. . . . . 6
⊢ 𝑈 = (𝑇 ↾s 𝑋) |
5 | 4 | submgmmgm 42323 |
. . . . 5
⊢ (𝑋 ∈ (SubMgm‘𝑇) → 𝑈 ∈ Mgm) |
6 | 5 | ad2antrr 764 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝑈 ∈ Mgm) |
7 | 3, 6 | jca 555 |
. . 3
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → (𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm)) |
8 | | eqid 2760 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
9 | | eqid 2760 |
. . . . . . . . 9
⊢
(Base‘𝑇) =
(Base‘𝑇) |
10 | 8, 9 | mgmhmf 42312 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
11 | 10 | adantl 473 |
. . . . . . 7
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
12 | | ffn 6206 |
. . . . . . 7
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹 Fn (Base‘𝑆)) |
14 | | simplr 809 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → ran 𝐹 ⊆ 𝑋) |
15 | | df-f 6053 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶𝑋 ↔ (𝐹 Fn (Base‘𝑆) ∧ ran 𝐹 ⊆ 𝑋)) |
16 | 13, 14, 15 | sylanbrc 701 |
. . . . 5
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹:(Base‘𝑆)⟶𝑋) |
17 | 4 | submgmbas 42324 |
. . . . . . 7
⊢ (𝑋 ∈ (SubMgm‘𝑇) → 𝑋 = (Base‘𝑈)) |
18 | 17 | ad2antrr 764 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝑋 = (Base‘𝑈)) |
19 | 18 | feq3d 6193 |
. . . . 5
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → (𝐹:(Base‘𝑆)⟶𝑋 ↔ 𝐹:(Base‘𝑆)⟶(Base‘𝑈))) |
20 | 16, 19 | mpbid 222 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑈)) |
21 | | eqid 2760 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘𝑆) |
22 | | eqid 2760 |
. . . . . . . . 9
⊢
(+g‘𝑇) = (+g‘𝑇) |
23 | 8, 21, 22 | mgmhmlin 42314 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
24 | 23 | 3expb 1114 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
25 | 24 | adantll 752 |
. . . . . 6
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
26 | 4, 22 | ressplusg 16215 |
. . . . . . . 8
⊢ (𝑋 ∈ (SubMgm‘𝑇) →
(+g‘𝑇) =
(+g‘𝑈)) |
27 | 26 | ad3antrrr 768 |
. . . . . . 7
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (+g‘𝑇) = (+g‘𝑈)) |
28 | 27 | oveqd 6831 |
. . . . . 6
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
29 | 25, 28 | eqtrd 2794 |
. . . . 5
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
30 | 29 | ralrimivva 3109 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
31 | 20, 30 | jca 555 |
. . 3
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → (𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)))) |
32 | | eqid 2760 |
. . . 4
⊢
(Base‘𝑈) =
(Base‘𝑈) |
33 | | eqid 2760 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
34 | 8, 32, 21, 33 | ismgmhm 42311 |
. . 3
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑈) ↔ ((𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm) ∧ (𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))))) |
35 | 7, 31, 34 | sylanbrc 701 |
. 2
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑈)) |
36 | 4 | resmgmhm2 42327 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑈) ∧ 𝑋 ∈ (SubMgm‘𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) |
37 | 36 | ancoms 468 |
. . 3
⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑈)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) |
38 | 37 | adantlr 753 |
. 2
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑈)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) |
39 | 35, 38 | impbida 913 |
1
⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ (𝑆 MgmHom 𝑈))) |