| Step | Hyp | Ref
| Expression |
| 1 | | mhmrcl2 18801 |
. . 3
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd) |
| 2 | | resmhm.u |
. . . 4
⊢ 𝑈 = (𝑆 ↾s 𝑋) |
| 3 | 2 | submmnd 18826 |
. . 3
⊢ (𝑋 ∈ (SubMnd‘𝑆) → 𝑈 ∈ Mnd) |
| 4 | 1, 3 | anim12ci 614 |
. 2
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝑈 ∈ Mnd ∧ 𝑇 ∈ Mnd)) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
| 7 | 5, 6 | mhmf 18802 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
| 8 | 5 | submss 18822 |
. . . . 5
⊢ (𝑋 ∈ (SubMnd‘𝑆) → 𝑋 ⊆ (Base‘𝑆)) |
| 9 | | fssres 6774 |
. . . . 5
⊢ ((𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ 𝑋 ⊆ (Base‘𝑆)) → (𝐹 ↾ 𝑋):𝑋⟶(Base‘𝑇)) |
| 10 | 7, 8, 9 | syl2an 596 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋):𝑋⟶(Base‘𝑇)) |
| 11 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → 𝑋 ⊆ (Base‘𝑆)) |
| 12 | 2, 5 | ressbas2 17283 |
. . . . . 6
⊢ (𝑋 ⊆ (Base‘𝑆) → 𝑋 = (Base‘𝑈)) |
| 13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → 𝑋 = (Base‘𝑈)) |
| 14 | 13 | feq2d 6722 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋):𝑋⟶(Base‘𝑇) ↔ (𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇))) |
| 15 | 10, 14 | mpbid 232 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇)) |
| 16 | | simpll 767 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
| 17 | 8 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝑆)) |
| 18 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
| 19 | 17, 18 | sseldd 3984 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ (Base‘𝑆)) |
| 20 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
| 21 | 17, 20 | sseldd 3984 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ (Base‘𝑆)) |
| 22 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑆) = (+g‘𝑆) |
| 23 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑇) = (+g‘𝑇) |
| 24 | 5, 22, 23 | mhmlin 18806 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 25 | 16, 19, 21, 24 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 26 | 22 | submcl 18825 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (SubMnd‘𝑆) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(+g‘𝑆)𝑦) ∈ 𝑋) |
| 27 | 26 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑋 ∈ (SubMnd‘𝑆) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(+g‘𝑆)𝑦) ∈ 𝑋) |
| 28 | 27 | adantll 714 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(+g‘𝑆)𝑦) ∈ 𝑋) |
| 29 | 28 | fvresd 6926 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (𝐹‘(𝑥(+g‘𝑆)𝑦))) |
| 30 | | fvres 6925 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘𝑥) = (𝐹‘𝑥)) |
| 31 | | fvres 6925 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘𝑦) = (𝐹‘𝑦)) |
| 32 | 30, 31 | oveqan12d 7450 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 33 | 32 | adantl 481 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 34 | 25, 29, 33 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦))) |
| 35 | 34 | ralrimivva 3202 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦))) |
| 36 | 2, 22 | ressplusg 17334 |
. . . . . . . . 9
⊢ (𝑋 ∈ (SubMnd‘𝑆) →
(+g‘𝑆) =
(+g‘𝑈)) |
| 37 | 36 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (+g‘𝑆) = (+g‘𝑈)) |
| 38 | 37 | oveqd 7448 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝑥(+g‘𝑆)𝑦) = (𝑥(+g‘𝑈)𝑦)) |
| 39 | 38 | fveqeq2d 6914 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ↔ ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)))) |
| 40 | 13, 39 | raleqbidv 3346 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (∀𝑦 ∈ 𝑋 ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)))) |
| 41 | 13, 40 | raleqbidv 3346 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑆)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ↔ ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)))) |
| 42 | 35, 41 | mpbid 232 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦))) |
| 43 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) |
| 44 | 43 | subm0cl 18824 |
. . . . . 6
⊢ (𝑋 ∈ (SubMnd‘𝑆) →
(0g‘𝑆)
∈ 𝑋) |
| 45 | 44 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (0g‘𝑆) ∈ 𝑋) |
| 46 | 45 | fvresd 6926 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(0g‘𝑆)) = (𝐹‘(0g‘𝑆))) |
| 47 | 2, 43 | subm0 18828 |
. . . . . 6
⊢ (𝑋 ∈ (SubMnd‘𝑆) →
(0g‘𝑆) =
(0g‘𝑈)) |
| 48 | 47 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (0g‘𝑆) = (0g‘𝑈)) |
| 49 | 48 | fveq2d 6910 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(0g‘𝑆)) = ((𝐹 ↾ 𝑋)‘(0g‘𝑈))) |
| 50 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) |
| 51 | 43, 50 | mhm0 18807 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
| 52 | 51 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
| 53 | 46, 49, 52 | 3eqtr3d 2785 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋)‘(0g‘𝑈)) = (0g‘𝑇)) |
| 54 | 15, 42, 53 | 3jca 1129 |
. 2
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → ((𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ∧ ((𝐹 ↾ 𝑋)‘(0g‘𝑈)) = (0g‘𝑇))) |
| 55 | | eqid 2737 |
. . 3
⊢
(Base‘𝑈) =
(Base‘𝑈) |
| 56 | | eqid 2737 |
. . 3
⊢
(+g‘𝑈) = (+g‘𝑈) |
| 57 | | eqid 2737 |
. . 3
⊢
(0g‘𝑈) = (0g‘𝑈) |
| 58 | 55, 6, 56, 23, 57, 50 | ismhm 18798 |
. 2
⊢ ((𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇) ↔ ((𝑈 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ ((𝐹 ↾ 𝑋):(Base‘𝑈)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑈)∀𝑦 ∈ (Base‘𝑈)((𝐹 ↾ 𝑋)‘(𝑥(+g‘𝑈)𝑦)) = (((𝐹 ↾ 𝑋)‘𝑥)(+g‘𝑇)((𝐹 ↾ 𝑋)‘𝑦)) ∧ ((𝐹 ↾ 𝑋)‘(0g‘𝑈)) = (0g‘𝑇)))) |
| 59 | 4, 54, 58 | sylanbrc 583 |
1
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇)) |