Step | Hyp | Ref
| Expression |
1 | | mhmrcl1 18221 |
. . 3
⊢ (𝐹 ∈ (𝑆 MndHom 𝑈) → 𝑆 ∈ Mnd) |
2 | | submrcl 18229 |
. . 3
⊢ (𝑋 ∈ (SubMnd‘𝑇) → 𝑇 ∈ Mnd) |
3 | 1, 2 | anim12i 616 |
. 2
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → (𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd)) |
4 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
5 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
6 | 4, 5 | mhmf 18223 |
. . . 4
⊢ (𝐹 ∈ (𝑆 MndHom 𝑈) → 𝐹:(Base‘𝑆)⟶(Base‘𝑈)) |
7 | | resmhm2.u |
. . . . . 6
⊢ 𝑈 = (𝑇 ↾s 𝑋) |
8 | 7 | submbas 18241 |
. . . . 5
⊢ (𝑋 ∈ (SubMnd‘𝑇) → 𝑋 = (Base‘𝑈)) |
9 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
10 | 9 | submss 18236 |
. . . . 5
⊢ (𝑋 ∈ (SubMnd‘𝑇) → 𝑋 ⊆ (Base‘𝑇)) |
11 | 8, 10 | eqsstrrd 3940 |
. . . 4
⊢ (𝑋 ∈ (SubMnd‘𝑇) → (Base‘𝑈) ⊆ (Base‘𝑇)) |
12 | | fss 6562 |
. . . 4
⊢ ((𝐹:(Base‘𝑆)⟶(Base‘𝑈) ∧ (Base‘𝑈) ⊆ (Base‘𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
13 | 6, 11, 12 | syl2an 599 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
14 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑆) = (+g‘𝑆) |
15 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑈) = (+g‘𝑈) |
16 | 4, 14, 15 | mhmlin 18225 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
17 | 16 | 3expb 1122 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
18 | 17 | adantlr 715 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
19 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑇) = (+g‘𝑇) |
20 | 7, 19 | ressplusg 16834 |
. . . . . . 7
⊢ (𝑋 ∈ (SubMnd‘𝑇) →
(+g‘𝑇) =
(+g‘𝑈)) |
21 | 20 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (+g‘𝑇) = (+g‘𝑈)) |
22 | 21 | oveqd 7230 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))) |
23 | 18, 22 | eqtr4d 2780 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
24 | 23 | ralrimivva 3112 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
25 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑆) = (0g‘𝑆) |
26 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑈) = (0g‘𝑈) |
27 | 25, 26 | mhm0 18226 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 MndHom 𝑈) → (𝐹‘(0g‘𝑆)) = (0g‘𝑈)) |
28 | 27 | adantr 484 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑈)) |
29 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) |
30 | 7, 29 | subm0 18242 |
. . . . 5
⊢ (𝑋 ∈ (SubMnd‘𝑇) →
(0g‘𝑇) =
(0g‘𝑈)) |
31 | 30 | adantl 485 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → (0g‘𝑇) = (0g‘𝑈)) |
32 | 28, 31 | eqtr4d 2780 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
33 | 13, 24, 32 | 3jca 1130 |
. 2
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇))) |
34 | 4, 9, 14, 19, 25, 29 | ismhm 18220 |
. 2
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇)))) |
35 | 3, 33, 34 | sylanbrc 586 |
1
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |