| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | imassrn 6089 | . . 3
⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹 | 
| 2 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝑁) =
(Base‘𝑁) | 
| 4 | 2, 3 | mgmhmf 18710 | . . . . 5
⊢ (𝐹 ∈ (𝑀 MgmHom 𝑁) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) | 
| 5 | 4 | adantr 480 | . . . 4
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) | 
| 6 | 5 | frnd 6744 | . . 3
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → ran 𝐹 ⊆ (Base‘𝑁)) | 
| 7 | 1, 6 | sstrid 3995 | . 2
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (𝐹 “ 𝑋) ⊆ (Base‘𝑁)) | 
| 8 |  | simpll 767 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝐹 ∈ (𝑀 MgmHom 𝑁)) | 
| 9 | 2 | submgmss 18718 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ (SubMgm‘𝑀) → 𝑋 ⊆ (Base‘𝑀)) | 
| 10 | 9 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → 𝑋 ⊆ (Base‘𝑀)) | 
| 11 | 10 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝑋 ⊆ (Base‘𝑀)) | 
| 12 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝑧 ∈ 𝑋) | 
| 13 | 11, 12 | sseldd 3984 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝑧 ∈ (Base‘𝑀)) | 
| 14 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝑥 ∈ 𝑋) | 
| 15 | 11, 14 | sseldd 3984 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝑥 ∈ (Base‘𝑀)) | 
| 16 |  | eqid 2737 | . . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 17 |  | eqid 2737 | . . . . . . . . . 10
⊢
(+g‘𝑁) = (+g‘𝑁) | 
| 18 | 2, 16, 17 | mgmhmlin 18712 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑧 ∈ (Base‘𝑀) ∧ 𝑥 ∈ (Base‘𝑀)) → (𝐹‘(𝑧(+g‘𝑀)𝑥)) = ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥))) | 
| 19 | 8, 13, 15, 18 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝐹‘(𝑧(+g‘𝑀)𝑥)) = ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥))) | 
| 20 | 5 | ffnd 6737 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → 𝐹 Fn (Base‘𝑀)) | 
| 21 | 20 | adantr 480 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → 𝐹 Fn (Base‘𝑀)) | 
| 22 | 16 | submgmcl 18720 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ (SubMgm‘𝑀) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧(+g‘𝑀)𝑥) ∈ 𝑋) | 
| 23 | 22 | 3expb 1121 | . . . . . . . . . 10
⊢ ((𝑋 ∈ (SubMgm‘𝑀) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑧(+g‘𝑀)𝑥) ∈ 𝑋) | 
| 24 | 23 | adantll 714 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑧(+g‘𝑀)𝑥) ∈ 𝑋) | 
| 25 |  | fnfvima 7253 | . . . . . . . . 9
⊢ ((𝐹 Fn (Base‘𝑀) ∧ 𝑋 ⊆ (Base‘𝑀) ∧ (𝑧(+g‘𝑀)𝑥) ∈ 𝑋) → (𝐹‘(𝑧(+g‘𝑀)𝑥)) ∈ (𝐹 “ 𝑋)) | 
| 26 | 21, 11, 24, 25 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝐹‘(𝑧(+g‘𝑀)𝑥)) ∈ (𝐹 “ 𝑋)) | 
| 27 | 19, 26 | eqeltrrd 2842 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ (𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋)) | 
| 28 | 27 | anassrs 467 | . . . . . 6
⊢ ((((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋)) | 
| 29 | 28 | ralrimiva 3146 | . . . . 5
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ 𝑧 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋)) | 
| 30 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘𝑧)(+g‘𝑁)𝑦) = ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥))) | 
| 31 | 30 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → (((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋))) | 
| 32 | 31 | ralima 7257 | . . . . . . 7
⊢ ((𝐹 Fn (Base‘𝑀) ∧ 𝑋 ⊆ (Base‘𝑀)) → (∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋))) | 
| 33 | 20, 10, 32 | syl2anc 584 | . . . . . 6
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋))) | 
| 34 | 33 | adantr 480 | . . . . 5
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ 𝑧 ∈ 𝑋) → (∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑧)(+g‘𝑁)(𝐹‘𝑥)) ∈ (𝐹 “ 𝑋))) | 
| 35 | 29, 34 | mpbird 257 | . . . 4
⊢ (((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) ∧ 𝑧 ∈ 𝑋) → ∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) | 
| 36 | 35 | ralrimiva 3146 | . . 3
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → ∀𝑧 ∈ 𝑋 ∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) | 
| 37 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑥 = (𝐹‘𝑧) → (𝑥(+g‘𝑁)𝑦) = ((𝐹‘𝑧)(+g‘𝑁)𝑦)) | 
| 38 | 37 | eleq1d 2826 | . . . . . 6
⊢ (𝑥 = (𝐹‘𝑧) → ((𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋))) | 
| 39 | 38 | ralbidv 3178 | . . . . 5
⊢ (𝑥 = (𝐹‘𝑧) → (∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋))) | 
| 40 | 39 | ralima 7257 | . . . 4
⊢ ((𝐹 Fn (Base‘𝑀) ∧ 𝑋 ⊆ (Base‘𝑀)) → (∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑧 ∈ 𝑋 ∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋))) | 
| 41 | 20, 10, 40 | syl2anc 584 | . . 3
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋) ↔ ∀𝑧 ∈ 𝑋 ∀𝑦 ∈ (𝐹 “ 𝑋)((𝐹‘𝑧)(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋))) | 
| 42 | 36, 41 | mpbird 257 | . 2
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)) | 
| 43 |  | mgmhmrcl 18707 | . . . . 5
⊢ (𝐹 ∈ (𝑀 MgmHom 𝑁) → (𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm)) | 
| 44 | 43 | simprd 495 | . . . 4
⊢ (𝐹 ∈ (𝑀 MgmHom 𝑁) → 𝑁 ∈ Mgm) | 
| 45 | 44 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → 𝑁 ∈ Mgm) | 
| 46 | 3, 17 | issubmgm 18715 | . . 3
⊢ (𝑁 ∈ Mgm → ((𝐹 “ 𝑋) ∈ (SubMgm‘𝑁) ↔ ((𝐹 “ 𝑋) ⊆ (Base‘𝑁) ∧ ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)))) | 
| 47 | 45, 46 | syl 17 | . 2
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → ((𝐹 “ 𝑋) ∈ (SubMgm‘𝑁) ↔ ((𝐹 “ 𝑋) ⊆ (Base‘𝑁) ∧ ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥(+g‘𝑁)𝑦) ∈ (𝐹 “ 𝑋)))) | 
| 48 | 7, 42, 47 | mpbir2and 713 | 1
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMgm‘𝑁)) |