mhmvlin

Description: Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	mhmvlin.b	$⊢ B = {Base}_{M}$
	mhmvlin.p	$⊢ \underset{˙}{+} = +_{M}$
	mhmvlin.q	$⊢ \underset{˙}{⨣} = +_{N}$
Assertion	mhmvlin	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F \circ (X {\underset{˙}{+}}_{f} Y) = (F \circ X) {\underset{˙}{⨣}}_{f} (F \circ Y)$

Proof

Step	Hyp	Ref	Expression
1		mhmvlin.b	$⊢ B = {Base}_{M}$
2		mhmvlin.p	$⊢ \underset{˙}{+} = +_{M}$
3		mhmvlin.q	$⊢ \underset{˙}{⨣} = +_{N}$
4		simpl1	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to F \in (M MndHom N)$
5		elmapi	$⊢ X \in (B^{I}) \to X : I ⟶ B$
6	5	3ad2ant2	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to X : I ⟶ B$
7	6	ffvelcdmda	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to X (y) \in B$
8		elmapi	$⊢ Y \in (B^{I}) \to Y : I ⟶ B$
9	8	3ad2ant3	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to Y : I ⟶ B$
10	9	ffvelcdmda	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to Y (y) \in B$
11	1 2 3	mhmlin	$⊢ (F \in (M MndHom N) \land X (y) \in B \land Y (y) \in B) \to F (X (y) \underset{˙}{+} Y (y)) = F (X (y)) \underset{˙}{⨣} F (Y (y))$
12	4 7 10 11	syl3anc	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to F (X (y) \underset{˙}{+} Y (y)) = F (X (y)) \underset{˙}{⨣} F (Y (y))$
13	12	mpteq2dva	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to (y \in I ⟼ F (X (y) \underset{˙}{+} Y (y))) = (y \in I ⟼ F (X (y)) \underset{˙}{⨣} F (Y (y)))$
14		mhmrcl1	$⊢ F \in (M MndHom N) \to M \in Mnd$
15	14	adantr	$⊢ (F \in (M MndHom N) \land y \in I) \to M \in Mnd$
16	15	3ad2antl1	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to M \in Mnd$
17	1 2	mndcl	$⊢ (M \in Mnd \land X (y) \in B \land Y (y) \in B) \to X (y) \underset{˙}{+} Y (y) \in B$
18	16 7 10 17	syl3anc	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to X (y) \underset{˙}{+} Y (y) \in B$
19		elmapex	$⊢ Y \in (B^{I}) \to (B \in V \land I \in V)$
20	19	simprd	$⊢ Y \in (B^{I}) \to I \in V$
21	20	3ad2ant3	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to I \in V$
22	6	feqmptd	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to X = (y \in I ⟼ X (y))$
23	9	feqmptd	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to Y = (y \in I ⟼ Y (y))$
24	21 7 10 22 23	offval2	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to X {\underset{˙}{+}}_{f} Y = (y \in I ⟼ X (y) \underset{˙}{+} Y (y))$
25		eqid	$⊢ {Base}_{N} = {Base}_{N}$
26	1 25	mhmf	$⊢ F \in (M MndHom N) \to F : B ⟶ {Base}_{N}$
27	26	3ad2ant1	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F : B ⟶ {Base}_{N}$
28	27	feqmptd	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F = (z \in B ⟼ F (z))$
29		fveq2	$⊢ z = X (y) \underset{˙}{+} Y (y) \to F (z) = F (X (y) \underset{˙}{+} Y (y))$
30	18 24 28 29	fmptco	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F \circ (X {\underset{˙}{+}}_{f} Y) = (y \in I ⟼ F (X (y) \underset{˙}{+} Y (y)))$
31		fvexd	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to F (X (y)) \in V$
32		fvexd	$⊢ ((F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \land y \in I) \to F (Y (y)) \in V$
33		fcompt	$⊢ (F : B ⟶ {Base}_{N} \land X : I ⟶ B) \to F \circ X = (y \in I ⟼ F (X (y)))$
34	27 6 33	syl2anc	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F \circ X = (y \in I ⟼ F (X (y)))$
35		fcompt	$⊢ (F : B ⟶ {Base}_{N} \land Y : I ⟶ B) \to F \circ Y = (y \in I ⟼ F (Y (y)))$
36	27 9 35	syl2anc	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F \circ Y = (y \in I ⟼ F (Y (y)))$
37	21 31 32 34 36	offval2	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to (F \circ X) {\underset{˙}{⨣}}_{f} (F \circ Y) = (y \in I ⟼ F (X (y)) \underset{˙}{⨣} F (Y (y)))$
38	13 30 37	3eqtr4d	$⊢ (F \in (M MndHom N) \land X \in (B^{I}) \land Y \in (B^{I})) \to F \circ (X {\underset{˙}{+}}_{f} Y) = (F \circ X) {\underset{˙}{⨣}}_{f} (F \circ Y)$

Metamath Proof Explorer

Theorem mhmvlin

Proof