Step | Hyp | Ref
| Expression |
1 | | mhmrcl2 17162 |
. . 3
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd) |
2 | | resmhm.u |
. . . 4
⊢ 𝑈 = (𝑆 ↾s 𝑋) |
3 | 2 | submmnd 17177 |
. . 3
⊢ (𝑋 ∈ (SubMnd‘𝑆) → 𝑈 ∈ Mnd) |
4 | 1, 3 | anim12ci 589 |
. 2
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝑈 ∈ Mnd ∧ 𝑇 ∈ Mnd)) |
5 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
6 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
7 | 5, 6 | mhmf 17163 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
8 | 5 | submss 17173 |
. . . . 5
⊢ (𝑋 ∈ (SubMnd‘𝑆) → 𝑋 ⊆ (Base‘𝑆)) |
9 | | fssres 5983 |
. . . . 5
⊢ ((𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ 𝑋 ⊆ (Base‘𝑆)) → (𝐹 ↾ 𝑋):𝑋⟶(Base‘𝑇)) |
10 | 7, 8, 9 | syl2an 493 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋):𝑋⟶(Base‘𝑇)) |
11 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → 𝑋 ⊆ (Base‘𝑆)) |
12 | 2, 5 | ressbas2 15758 |
. . . . . 6
⊢ (𝑋 ⊆ (Base‘𝑆) → 𝑋 = (Base‘𝑈)) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → 𝑋 = (Base‘𝑈)) |
14 | 13 | feq2d 5944 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋):𝑋⟶(Base‘𝑇) ↔ (𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇))) |
15 | 10, 14 | mpbid 221 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇)) |
16 | | simpll 786 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
17 | 8 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝑆)) |
18 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
19 | 17, 18 | sseldd 3569 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ (Base‘𝑆)) |
20 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
21 | 17, 20 | sseldd 3569 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ (Base‘𝑆)) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝑆) = (+g‘𝑆) |
23 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝑇) = (+g‘𝑇) |
24 | 5, 22, 23 | mhmlin 17165 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
25 | 16, 19, 21, 24 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
26 | 22 | submcl 17176 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (SubMnd‘𝑆) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(+g‘𝑆)𝑦) ∈ 𝑋) |
27 | 26 | 3expb 1258 |
. . . . . . . 8
⊢ ((𝑋 ∈ (SubMnd‘𝑆) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(+g‘𝑆)𝑦) ∈ 𝑋) |
28 | 27 | adantll 746 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(+g‘𝑆)𝑦) ∈ 𝑋) |
29 | | fvres 6117 |
. . . . . . 7
⊢ ((𝑥(+g‘𝑆)𝑦) ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (𝐹‘(𝑥(+g‘𝑆)𝑦))) |
30 | 28, 29 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (𝐹‘(𝑥(+g‘𝑆)𝑦))) |
31 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘𝑥) = (𝐹‘𝑥)) |
32 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘𝑦) = (𝐹‘𝑦)) |
33 | 31, 32 | oveqan12d 6568 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
34 | 33 | adantl 481 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
35 | 25, 30, 34 | 3eqtr4d 2654 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦))) |
36 | 35 | ralrimivva 2954 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦))) |
37 | 2, 22 | ressplusg 15818 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (SubMnd‘𝑆) →
(+g‘𝑆) =
(+g‘𝑈)) |
38 | 37 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (+g‘𝑆) = (+g‘𝑈)) |
39 | 38 | oveqd 6566 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝑥(+g‘𝑆)𝑦) = (𝑥(+g‘𝑈)𝑦)) |
40 | 39 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦))) |
41 | 40 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ↔ ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)))) |
42 | 13, 41 | raleqbidv 3129 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (∀𝑦 ∈ 𝑋 ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)))) |
43 | 13, 42 | raleqbidv 3129 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ↔ ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)))) |
44 | 36, 43 | mpbid 221 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦))) |
45 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
46 | 45 | subm0cl 17175 |
. . . . . 6
⊢ (𝑋 ∈ (SubMnd‘𝑆) →
(0g‘𝑆)
∈ 𝑋) |
47 | 46 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (0g‘𝑆) ∈ 𝑋) |
48 | | fvres 6117 |
. . . . 5
⊢
((0g‘𝑆) ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘(0g‘𝑆)) = (𝐹‘(0g‘𝑆))) |
49 | 47, 48 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(0g‘𝑆)) = (𝐹‘(0g‘𝑆))) |
50 | 2, 45 | subm0 17179 |
. . . . . 6
⊢ (𝑋 ∈ (SubMnd‘𝑆) →
(0g‘𝑆) =
(0g‘𝑈)) |
51 | 50 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (0g‘𝑆) = (0g‘𝑈)) |
52 | 51 | fveq2d 6107 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(0g‘𝑆)) = ((𝐹 ↾ 𝑋)‘(0g‘𝑈))) |
53 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) |
54 | 45, 53 | mhm0 17166 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
55 | 54 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
56 | 49, 52, 55 | 3eqtr3d 2652 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(0g‘𝑈)) = (0g‘𝑇)) |
57 | 15, 44, 56 | 3jca 1235 |
. 2
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ∧ ((𝐹 ↾ 𝑋)‘(0g‘𝑈)) = (0g‘𝑇))) |
58 | | eqid 2610 |
. . 3
⊢
(Base‘𝑈) =
(Base‘𝑈) |
59 | | eqid 2610 |
. . 3
⊢
(+g‘𝑈) = (+g‘𝑈) |
60 | | eqid 2610 |
. . 3
⊢
(0g‘𝑈) = (0g‘𝑈) |
61 | 58, 6, 59, 23, 60, 53 | ismhm 17160 |
. 2
⊢ ((𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇) ↔ ((𝑈 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ ((𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ∧ ((𝐹 ↾ 𝑋)‘(0g‘𝑈)) = (0g‘𝑇)))) |
62 | 4, 57, 61 | sylanbrc 695 |
1
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇)) |