mhmima

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

		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		simpl	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F \in (M MndHom N)$
21		eqidd	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to +_{M} = +_{M}$
22		eqidd	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to +_{N} = +_{N}$
23		eqid	$⊢ +_{M} = +_{M}$
24	23	submcl	$⊢ (X \in SubMnd (M) \land z \in X \land x \in X) \to z +_{M} x \in X$
25	24	3adant1l	$⊢ ((F \in (M MndHom N) \land X \in SubMnd (M)) \land z \in X \land x \in X) \to z +_{M} x \in X$
26	20 14 21 22 25	mhmimalem	$⊢ (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]$
27		mhmrcl2	$⊢ F \in (M MndHom N) \to N \in Mnd$
28	27	adantr	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to N \in Mnd$
29		eqid	$⊢ +_{N} = +_{N}$
30	3 9 29	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]))$
31	28 30	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]))$
32	7 19 26 31	mpbir3and	$⊢ (F \in (M MndHom N) \land X \in SubMnd (M)) \to F [X] \in SubMnd (N)$

Metamath Proof Explorer

Theorem mhmima

Proof