mgmhmima

Description: The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020)

		Ref	Expression
	Assertion	mgmhmima	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to F [X] \in SubMgm (N)$

Proof

Step	Hyp	Ref	Expression
1		imassrn	$⊢ F [X] \subseteq ran F$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ {Base}_{N} = {Base}_{N}$
4	2 3	mgmhmf	$⊢ F \in (M MgmHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
5	4	adantr	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to F : {Base}_{M} ⟶ {Base}_{N}$
6	5	frnd	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to ran F \subseteq {Base}_{N}$
7	1 6	sstrid	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to F [X] \subseteq {Base}_{N}$
8		simpll	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to F \in (M MgmHom N)$
9	2	submgmss	$⊢ X \in SubMgm (M) \to X \subseteq {Base}_{M}$
10	9	adantl	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to X \subseteq {Base}_{M}$
11	10	adantr	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to X \subseteq {Base}_{M}$
12		simprl	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to z \in X$
13	11 12	sseldd	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to z \in {Base}_{M}$
14		simprr	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to x \in X$
15	11 14	sseldd	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to x \in {Base}_{M}$
16		eqid	$⊢ +_{M} = +_{M}$
17		eqid	$⊢ +_{N} = +_{N}$
18	2 16 17	mgmhmlin	$⊢ (F \in (M MgmHom N) \land z \in {Base}_{M} \land x \in {Base}_{M}) \to F (z +_{M} x) = F (z) +_{N} F (x)$
19	8 13 15 18	syl3anc	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to F (z +_{M} x) = F (z) +_{N} F (x)$
20	5	ffnd	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to F Fn {Base}_{M}$
21	20	adantr	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to F Fn {Base}_{M}$
22	16	submgmcl	$⊢ (X \in SubMgm (M) \land z \in X \land x \in X) \to z +_{M} x \in X$
23	22	3expb	$⊢ (X \in SubMgm (M) \land (z \in X \land x \in X)) \to z +_{M} x \in X$
24	23	adantll	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to z +_{M} x \in X$
25		fnfvima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M} \land z +_{M} x \in X) \to F (z +_{M} x) \in F [X]$
26	21 11 24 25	syl3anc	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to F (z +_{M} x) \in F [X]$
27	19 26	eqeltrrd	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land (z \in X \land x \in X)) \to F (z) +_{N} F (x) \in F [X]$
28	27	anassrs	$⊢ (((F \in (M MgmHom N) \land X \in SubMgm (M)) \land z \in X) \land x \in X) \to F (z) +_{N} F (x) \in F [X]$
29	28	ralrimiva	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land z \in X) \to \forall x \in X F (z) +_{N} F (x) \in F [X]$
30		oveq2	$⊢ y = F (x) \to F (z) +_{N} y = F (z) +_{N} F (x)$
31	30	eleq1d	$⊢ y = F (x) \to (F (z) +_{N} y \in F [X] \leftrightarrow F (z) +_{N} F (x) \in F [X])$
32	31	ralima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M}) \to (\forall y \in F [X] F (z) +_{N} y \in F [X] \leftrightarrow \forall x \in X F (z) +_{N} F (x) \in F [X])$
33	20 10 32	syl2anc	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to (\forall y \in F [X] F (z) +_{N} y \in F [X] \leftrightarrow \forall x \in X F (z) +_{N} F (x) \in F [X])$
34	33	adantr	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land z \in X) \to (\forall y \in F [X] F (z) +_{N} y \in F [X] \leftrightarrow \forall x \in X F (z) +_{N} F (x) \in F [X])$
35	29 34	mpbird	$⊢ ((F \in (M MgmHom N) \land X \in SubMgm (M)) \land z \in X) \to \forall y \in F [X] F (z) +_{N} y \in F [X]$
36	35	ralrimiva	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X]$
37		oveq1	$⊢ x = F (z) \to x +_{N} y = F (z) +_{N} y$
38	37	eleq1d	$⊢ x = F (z) \to (x +_{N} y \in F [X] \leftrightarrow F (z) +_{N} y \in F [X])$
39	38	ralbidv	$⊢ x = F (z) \to (\forall y \in F [X] x +_{N} y \in F [X] \leftrightarrow \forall y \in F [X] F (z) +_{N} y \in F [X])$
40	39	ralima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M}) \to (\forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X] \leftrightarrow \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X])$
41	20 10 40	syl2anc	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to (\forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X] \leftrightarrow \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X])$
42	36 41	mpbird	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]$
43		mgmhmrcl	$⊢ F \in (M MgmHom N) \to (M \in Mgm \land N \in Mgm)$
44	43	simprd	$⊢ F \in (M MgmHom N) \to N \in Mgm$
45	44	adantr	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to N \in Mgm$
46	3 17	issubmgm	$⊢ N \in Mgm \to (F [X] \in SubMgm (N) \leftrightarrow (F [X] \subseteq {Base}_{N} \land \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]))$
47	45 46	syl	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to (F [X] \in SubMgm (N) \leftrightarrow (F [X] \subseteq {Base}_{N} \land \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]))$
48	7 42 47	mpbir2and	$⊢ (F \in (M MgmHom N) \land X \in SubMgm (M)) \to F [X] \in SubMgm (N)$

Metamath Proof Explorer

Theorem mgmhmima

Proof