Step | Hyp | Ref
| Expression |
1 | | mhmrcl1 17338 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd) |
2 | 1 | adantl 482 |
. . . 4
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝑆 ∈ Mnd) |
3 | | resmhm2.u |
. . . . . 6
⊢ 𝑈 = (𝑇 ↾s 𝑋) |
4 | 3 | submmnd 17354 |
. . . . 5
⊢ (𝑋 ∈ (SubMnd‘𝑇) → 𝑈 ∈ Mnd) |
5 | 4 | ad2antrr 762 |
. . . 4
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝑈 ∈ Mnd) |
6 | 2, 5 | jca 554 |
. . 3
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → (𝑆 ∈ Mnd ∧ 𝑈 ∈ Mnd)) |
7 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
8 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑇) =
(Base‘𝑇) |
9 | 7, 8 | mhmf 17340 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
10 | 9 | adantl 482 |
. . . . . . 7
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
11 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝐹 Fn (Base‘𝑆)) |
13 | | simplr 792 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → ran 𝐹 ⊆ 𝑋) |
14 | | df-f 5892 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶𝑋 ↔ (𝐹 Fn (Base‘𝑆) ∧ ran 𝐹 ⊆ 𝑋)) |
15 | 12, 13, 14 | sylanbrc 698 |
. . . . 5
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝐹:(Base‘𝑆)⟶𝑋) |
16 | 3 | submbas 17355 |
. . . . . . 7
⊢ (𝑋 ∈ (SubMnd‘𝑇) → 𝑋 = (Base‘𝑈)) |
17 | 16 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝑋 = (Base‘𝑈)) |
18 | 17 | feq3d 6032 |
. . . . 5
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → (𝐹:(Base‘𝑆)⟶𝑋 ↔ 𝐹:(Base‘𝑆)⟶(Base‘𝑈))) |
19 | 15, 18 | mpbid 222 |
. . . 4
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑈)) |
20 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘𝑆) |
21 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝑇) = (+g‘𝑇) |
22 | 7, 20, 21 | mhmlin 17342 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
23 | 22 | 3expb 1266 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
24 | 23 | adantll 750 |
. . . . . 6
⊢ ((((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
25 | 3, 21 | ressplusg 15993 |
. . . . . . . 8
⊢ (𝑋 ∈ (SubMnd‘𝑇) →
(+g‘𝑇) =
(+g‘𝑈)) |
26 | 25 | ad3antrrr 766 |
. . . . . . 7
⊢ ((((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (+g‘𝑇) = (+g‘𝑈)) |
27 | 26 | oveqd 6667 |
. . . . . 6
⊢ ((((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
28 | 24, 27 | eqtrd 2656 |
. . . . 5
⊢ ((((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
29 | 28 | ralrimivva 2971 |
. . . 4
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
30 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
31 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝑇) = (0g‘𝑇) |
32 | 30, 31 | mhm0 17343 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
33 | 32 | adantl 482 |
. . . . 5
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
34 | 3, 31 | subm0 17356 |
. . . . . 6
⊢ (𝑋 ∈ (SubMnd‘𝑇) →
(0g‘𝑇) =
(0g‘𝑈)) |
35 | 34 | ad2antrr 762 |
. . . . 5
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → (0g‘𝑇) = (0g‘𝑈)) |
36 | 33, 35 | eqtrd 2656 |
. . . 4
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑈)) |
37 | 19, 29, 36 | 3jca 1242 |
. . 3
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → (𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑈))) |
38 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑈) =
(Base‘𝑈) |
39 | | eqid 2622 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
40 | | eqid 2622 |
. . . 4
⊢
(0g‘𝑈) = (0g‘𝑈) |
41 | 7, 38, 20, 39, 30, 40 | ismhm 17337 |
. . 3
⊢ (𝐹 ∈ (𝑆 MndHom 𝑈) ↔ ((𝑆 ∈ Mnd ∧ 𝑈 ∈ Mnd) ∧ (𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑈)))) |
42 | 6, 37, 41 | sylanbrc 698 |
. 2
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑈)) |
43 | 3 | resmhm2 17360 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
44 | 43 | ancoms 469 |
. . 3
⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ 𝐹 ∈ (𝑆 MndHom 𝑈)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
45 | 44 | adantlr 751 |
. 2
⊢ (((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) ∧ 𝐹 ∈ (𝑆 MndHom 𝑈)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
46 | 42, 45 | impbida 877 |
1
⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈))) |