Step | Hyp | Ref
| Expression |
1 | | mgmhmrcl 41571 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm)) |
2 | 1 | simpld 474 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝑆 ∈ Mgm) |
3 | 2 | adantl 481 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝑆 ∈ Mgm) |
4 | | resmgmhm2.u |
. . . . . 6
⊢ 𝑈 = (𝑇 ↾s 𝑋) |
5 | 4 | submgmmgm 41585 |
. . . . 5
⊢ (𝑋 ∈ (SubMgm‘𝑇) → 𝑈 ∈ Mgm) |
6 | 5 | ad2antrr 758 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝑈 ∈ Mgm) |
7 | 3, 6 | jca 553 |
. . 3
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → (𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm)) |
8 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
9 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑇) =
(Base‘𝑇) |
10 | 8, 9 | mgmhmf 41574 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
11 | 10 | adantl 481 |
. . . . . . 7
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
12 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹 Fn (Base‘𝑆)) |
14 | | simplr 788 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → ran 𝐹 ⊆ 𝑋) |
15 | | df-f 5808 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶𝑋 ↔ (𝐹 Fn (Base‘𝑆) ∧ ran 𝐹 ⊆ 𝑋)) |
16 | 13, 14, 15 | sylanbrc 695 |
. . . . 5
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹:(Base‘𝑆)⟶𝑋) |
17 | 4 | submgmbas 41586 |
. . . . . . 7
⊢ (𝑋 ∈ (SubMgm‘𝑇) → 𝑋 = (Base‘𝑈)) |
18 | 17 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝑋 = (Base‘𝑈)) |
19 | 18 | feq3d 5945 |
. . . . 5
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → (𝐹:(Base‘𝑆)⟶𝑋 ↔ 𝐹:(Base‘𝑆)⟶(Base‘𝑈))) |
20 | 16, 19 | mpbid 221 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑈)) |
21 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘𝑆) |
22 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝑇) = (+g‘𝑇) |
23 | 8, 21, 22 | mgmhmlin 41576 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
24 | 23 | 3expb 1258 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
25 | 24 | adantll 746 |
. . . . . 6
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
26 | 4, 22 | ressplusg 15818 |
. . . . . . . 8
⊢ (𝑋 ∈ (SubMgm‘𝑇) →
(+g‘𝑇) =
(+g‘𝑈)) |
27 | 26 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (+g‘𝑇) = (+g‘𝑈)) |
28 | 27 | oveqd 6566 |
. . . . . 6
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
29 | 25, 28 | eqtrd 2644 |
. . . . 5
⊢ ((((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
30 | 29 | ralrimivva 2954 |
. . . 4
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
31 | 20, 30 | jca 553 |
. . 3
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → (𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)))) |
32 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑈) =
(Base‘𝑈) |
33 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
34 | 8, 32, 21, 33 | ismgmhm 41573 |
. . 3
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑈) ↔ ((𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm) ∧ (𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))))) |
35 | 7, 31, 34 | sylanbrc 695 |
. 2
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑈)) |
36 | 4 | resmgmhm2 41589 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑈) ∧ 𝑋 ∈ (SubMgm‘𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) |
37 | 36 | ancoms 468 |
. . 3
⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑈)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) |
38 | 37 | adantlr 747 |
. 2
⊢ (((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MgmHom 𝑈)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) |
39 | 35, 38 | impbida 873 |
1
⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ (𝑆 MgmHom 𝑈))) |