mhmima

Description: The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Assertion	mhmima	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F [X] \in SubMnd (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	mhmf	$⊢ F \in (M MndHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
5	4	adantr	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F : {Base}_{M} ⟶ {Base}_{N}$
6	5	frnd	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to ran F \subseteq {Base}_{N}$
7	1 6	sstrid	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F [X] \subseteq {Base}_{N}$
8		eqid	$⊢ 0_{M} = 0_{M}$
9		eqid	$⊢ 0_{N} = 0_{N}$
10	8 9	mhm0	$⊢ F \in (M MndHom N) \to F (0_{M}) = 0_{N}$
11	10	adantr	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F (0_{M}) = 0_{N}$
12	5	ffnd	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F Fn {Base}_{M}$
13	2	submss	$⊢ X \in SubMnd (M) \to X \subseteq {Base}_{M}$
14	13	adantl	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to X \subseteq {Base}_{M}$
15	8	subm0cl	$⊢ X \in SubMnd (M) \to 0_{M} \in X$
16	15	adantl	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to 0_{M} \in X$
17		fnfvima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M} \land 0_{M} \in X) \to F (0_{M}) \in F [X]$
18	12 14 16 17	syl3anc	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F (0_{M}) \in F [X]$
19	11 18	eqeltrrd	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to 0_{N} \in F [X]$
20		simpll	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to F \in (M MndHom N)$
21	14	adantr	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to X \subseteq {Base}_{M}$
22		simprl	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to z \in X$
23	21 22	sseldd	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to z \in {Base}_{M}$
24		simprr	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to x \in X$
25	21 24	sseldd	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to x \in {Base}_{M}$
26		eqid	$⊢ +_{M} = +_{M}$
27		eqid	$⊢ +_{N} = +_{N}$
28	2 26 27	mhmlin	$⊢ (F \in (M MndHom N) \land z \in {Base}_{M} \land x \in {Base}_{M}) \to F (z +_{M} x) = F (z) +_{N} F (x)$
29	20 23 25 28	syl3anc	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to F (z +_{M} x) = F (z) +_{N} F (x)$
30	12	adantr	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to F Fn {Base}_{M}$
31	26	submcl	$⊢ (X \in SubMnd (M) \land z \in X \land x \in X) \to z +_{M} x \in X$
32	31	3expb	$⊢ (X \in SubMnd (M) \land (z \in X \land x \in X)) \to z +_{M} x \in X$
33	32	adantll	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to z +_{M} x \in X$
34		fnfvima	$⊢ (F Fn {Base}_{M} \land X \subseteq {Base}_{M} \land z +_{M} x \in X) \to F (z +_{M} x) \in F [X]$
35	30 21 33 34	syl3anc	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to F (z +_{M} x) \in F [X]$
36	29 35	eqeltrrd	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land (z \in X \land x \in X)) \to F (z) +_{N} F (x) \in F [X]$
37	36	anassrs	$⊢ (((F \in (M MndHom N) \land X \in SubMnd (M)) \land z \in X) \land x \in X) \to F (z) +_{N} F (x) \in F [X]$
38	37	ralrimiva	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land z \in X) \to \forall x \in X F (z) +_{N} F (x) \in F [X]$
39		oveq2	$⊢ y = F (x) \to F (z) +_{N} y = F (z) +_{N} F (x)$
40	39	eleq1d	$⊢ y = F (x) \to (F (z) +_{N} y \in F [X] \leftrightarrow F (z) +_{N} F (x) \in F [X])$
41	40	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])$
42	12 14 41	syl2anc	$⊢ (F \in (M MndHom N) \land X \in SubMnd (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])$
43	42	adantr	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (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])$
44	38 43	mpbird	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land z \in X) \to \forall y \in F [X] F (z) +_{N} y \in F [X]$
45	44	ralrimiva	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to \forall z \in X \forall y \in F [X] F (z) +_{N} y \in F [X]$
46		oveq1	$⊢ x = F (z) \to x +_{N} y = F (z) +_{N} y$
47	46	eleq1d	$⊢ x = F (z) \to (x +_{N} y \in F [X] \leftrightarrow F (z) +_{N} y \in F [X])$
48	47	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])$
49	48	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])$
50	12 14 49	syl2anc	$⊢ (F \in (M MndHom N) \land X \in SubMnd (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])$
51	45 50	mpbird	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]$
52		mhmrcl2	$⊢ F \in (M MndHom N) \to N \in Mnd$
53	52	adantr	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to N \in Mnd$
54	3 9 27	issubm	$⊢ N \in Mnd \to (F [X] \in SubMnd (N) \leftrightarrow (F [X] \subseteq {Base}_{N} \land 0_{N} \in F [X] \land \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]))$
55	53 54	syl	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to (F [X] \in SubMnd (N) \leftrightarrow (F [X] \subseteq {Base}_{N} \land 0_{N} \in F [X] \land \forall x \in F [X] \forall y \in F [X] x +_{N} y \in F [X]))$
56	7 19 51 55	mpbir3and	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F [X] \in SubMnd (N)$

Metamath Proof Explorer

Theorem mhmima

Proof