Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
3 | 1, 2 | mhmf 17163 |
. . 3
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) |
4 | | cntzmhm.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝐺) |
5 | 1, 4 | cntzssv 17584 |
. . . 4
⊢ (𝑍‘𝑆) ⊆ (Base‘𝐺) |
6 | 5 | sseli 3564 |
. . 3
⊢ (𝐴 ∈ (𝑍‘𝑆) → 𝐴 ∈ (Base‘𝐺)) |
7 | | ffvelrn 6265 |
. . 3
⊢ ((𝐹:(Base‘𝐺)⟶(Base‘𝐻) ∧ 𝐴 ∈ (Base‘𝐺)) → (𝐹‘𝐴) ∈ (Base‘𝐻)) |
8 | 3, 6, 7 | syl2an 493 |
. 2
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (Base‘𝐻)) |
9 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
10 | 9, 4 | cntzi 17585 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝐴(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)𝐴)) |
11 | 10 | adantll 746 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐴(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)𝐴)) |
12 | 11 | fveq2d 6107 |
. . . . 5
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐹‘(𝐴(+g‘𝐺)𝑥)) = (𝐹‘(𝑥(+g‘𝐺)𝐴))) |
13 | | simpll 786 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ (𝐺 MndHom 𝐻)) |
14 | 6 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ (Base‘𝐺)) |
15 | 1, 4 | cntzrcl 17583 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑍‘𝑆) → (𝐺 ∈ V ∧ 𝑆 ⊆ (Base‘𝐺))) |
16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐺 ∈ V ∧ 𝑆 ⊆ (Base‘𝐺))) |
17 | 16 | simprd 478 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → 𝑆 ⊆ (Base‘𝐺)) |
18 | 17 | sselda 3568 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐺)) |
19 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝐻) = (+g‘𝐻) |
20 | 1, 9, 19 | mhmlin 17165 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝐹‘(𝐴(+g‘𝐺)𝑥)) = ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥))) |
21 | 13, 14, 18, 20 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐹‘(𝐴(+g‘𝐺)𝑥)) = ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥))) |
22 | 1, 9, 19 | mhmlin 17165 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝐴 ∈ (Base‘𝐺)) → (𝐹‘(𝑥(+g‘𝐺)𝐴)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴))) |
23 | 13, 18, 14, 22 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐹‘(𝑥(+g‘𝐺)𝐴)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴))) |
24 | 12, 21, 23 | 3eqtr3d 2652 |
. . . 4
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴))) |
25 | 24 | ralrimiva 2949 |
. . 3
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → ∀𝑥 ∈ 𝑆 ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴))) |
26 | 3 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → 𝐹:(Base‘𝐺)⟶(Base‘𝐻)) |
27 | | ffn 5958 |
. . . . 5
⊢ (𝐹:(Base‘𝐺)⟶(Base‘𝐻) → 𝐹 Fn (Base‘𝐺)) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → 𝐹 Fn (Base‘𝐺)) |
29 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘𝐴)(+g‘𝐻)𝑦) = ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥))) |
30 | | oveq1 6556 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦(+g‘𝐻)(𝐹‘𝐴)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴))) |
31 | 29, 30 | eqeq12d 2625 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝑥) → (((𝐹‘𝐴)(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)(𝐹‘𝐴)) ↔ ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴)))) |
32 | 31 | ralima 6402 |
. . . 4
⊢ ((𝐹 Fn (Base‘𝐺) ∧ 𝑆 ⊆ (Base‘𝐺)) → (∀𝑦 ∈ (𝐹 “ 𝑆)((𝐹‘𝐴)(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)(𝐹‘𝐴)) ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴)))) |
33 | 28, 17, 32 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (∀𝑦 ∈ (𝐹 “ 𝑆)((𝐹‘𝐴)(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)(𝐹‘𝐴)) ↔ ∀𝑥 ∈ 𝑆 ((𝐹‘𝐴)(+g‘𝐻)(𝐹‘𝑥)) = ((𝐹‘𝑥)(+g‘𝐻)(𝐹‘𝐴)))) |
34 | 25, 33 | mpbird 246 |
. 2
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → ∀𝑦 ∈ (𝐹 “ 𝑆)((𝐹‘𝐴)(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)(𝐹‘𝐴))) |
35 | | imassrn 5396 |
. . . 4
⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹 |
36 | | frn 5966 |
. . . . 5
⊢ (𝐹:(Base‘𝐺)⟶(Base‘𝐻) → ran 𝐹 ⊆ (Base‘𝐻)) |
37 | 26, 36 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → ran 𝐹 ⊆ (Base‘𝐻)) |
38 | 35, 37 | syl5ss 3579 |
. . 3
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹 “ 𝑆) ⊆ (Base‘𝐻)) |
39 | | cntzmhm.y |
. . . 4
⊢ 𝑌 = (Cntz‘𝐻) |
40 | 2, 19, 39 | elcntz 17578 |
. . 3
⊢ ((𝐹 “ 𝑆) ⊆ (Base‘𝐻) → ((𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆)) ↔ ((𝐹‘𝐴) ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ (𝐹 “ 𝑆)((𝐹‘𝐴)(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)(𝐹‘𝐴))))) |
41 | 38, 40 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → ((𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆)) ↔ ((𝐹‘𝐴) ∈ (Base‘𝐻) ∧ ∀𝑦 ∈ (𝐹 “ 𝑆)((𝐹‘𝐴)(+g‘𝐻)𝑦) = (𝑦(+g‘𝐻)(𝐹‘𝐴))))) |
42 | 8, 34, 41 | mpbir2and 959 |
1
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆))) |