mhmvlin - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mhmvlin		Structured version Visualization version GIF version

Theorem mhmvlin 21899

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

**Hypotheses**
Ref	Expression
mhmvlin.b	⊢ 𝐵 = (Base‘𝑀)
mhmvlin.p	⊢ + = (+_g‘𝑀)
mhmvlin.q	⊢ ⨣ = (+_g‘𝑁)

**Assertion**
Ref	Expression
mhmvlin	⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝐹 ∘ (𝑋 ∘_f + 𝑌)) = ((𝐹 ∘ 𝑋) ∘_f ⨣ (𝐹 ∘ 𝑌)))

Proof of Theorem mhmvlin Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1192	. . . 4 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → 𝐹 ∈ (𝑀 MndHom 𝑁))
2		elmapi 8843	. . . . . 6 ⊢ (𝑋 ∈ (𝐵 ↑_m 𝐼) → 𝑋:𝐼⟶𝐵)
3	2	3ad2ant2 1135	. . . . 5 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝑋:𝐼⟶𝐵)
4	3	ffvelcdmda 7087	. . . 4 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝑋‘𝑦) ∈ 𝐵)
5		elmapi 8843	. . . . . 6 ⊢ (𝑌 ∈ (𝐵 ↑_m 𝐼) → 𝑌:𝐼⟶𝐵)
6	5	3ad2ant3 1136	. . . . 5 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝑌:𝐼⟶𝐵)
7	6	ffvelcdmda 7087	. . . 4 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝑌‘𝑦) ∈ 𝐵)
8		mhmvlin.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑀)
9		mhmvlin.p	. . . . 5 ⊢ + = (+_g‘𝑀)
10		mhmvlin.q	. . . . 5 ⊢ ⨣ = (+_g‘𝑁)
11	8, 9, 10	mhmlin 18679	. . . 4 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ (𝑋‘𝑦) ∈ 𝐵 ∧ (𝑌‘𝑦) ∈ 𝐵) → (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦))) = ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦))))
12	1, 4, 7, 11	syl3anc 1372	. . 3 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦))) = ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦))))
13	12	mpteq2dva 5249	. 2 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝑦 ∈ 𝐼 ↦ (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦)))) = (𝑦 ∈ 𝐼 ↦ ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦)))))
14		mhmrcl1 18675	. . . . . 6 ⊢ (𝐹 ∈ (𝑀 MndHom 𝑁) → 𝑀 ∈ Mnd)
15	14	adantr 482	. . . . 5 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑦 ∈ 𝐼) → 𝑀 ∈ Mnd)
16	15	3ad2antl1 1186	. . . 4 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → 𝑀 ∈ Mnd)
17	8, 9	mndcl 18633	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ (𝑋‘𝑦) ∈ 𝐵 ∧ (𝑌‘𝑦) ∈ 𝐵) → ((𝑋‘𝑦) + (𝑌‘𝑦)) ∈ 𝐵)
18	16, 4, 7, 17	syl3anc 1372	. . 3 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → ((𝑋‘𝑦) + (𝑌‘𝑦)) ∈ 𝐵)
19		elmapex 8842	. . . . . 6 ⊢ (𝑌 ∈ (𝐵 ↑_m 𝐼) → (𝐵 ∈ V ∧ 𝐼 ∈ V))
20	19	simprd 497	. . . . 5 ⊢ (𝑌 ∈ (𝐵 ↑_m 𝐼) → 𝐼 ∈ V)
21	20	3ad2ant3 1136	. . . 4 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝐼 ∈ V)
22	3	feqmptd 6961	. . . 4 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝑋 = (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)))
23	6	feqmptd 6961	. . . 4 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝑌 = (𝑦 ∈ 𝐼 ↦ (𝑌‘𝑦)))
24	21, 4, 7, 22, 23	offval2 7690	. . 3 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝑋 ∘_f + 𝑌) = (𝑦 ∈ 𝐼 ↦ ((𝑋‘𝑦) + (𝑌‘𝑦))))
25		eqid 2733	. . . . . 6 ⊢ (Base‘𝑁) = (Base‘𝑁)
26	8, 25	mhmf 18677	. . . . 5 ⊢ (𝐹 ∈ (𝑀 MndHom 𝑁) → 𝐹:𝐵⟶(Base‘𝑁))
27	26	3ad2ant1 1134	. . . 4 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝐹:𝐵⟶(Base‘𝑁))
28	27	feqmptd 6961	. . 3 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → 𝐹 = (𝑧 ∈ 𝐵 ↦ (𝐹‘𝑧)))
29		fveq2 6892	. . 3 ⊢ (𝑧 = ((𝑋‘𝑦) + (𝑌‘𝑦)) → (𝐹‘𝑧) = (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦))))
30	18, 24, 28, 29	fmptco 7127	. 2 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝐹 ∘ (𝑋 ∘_f + 𝑌)) = (𝑦 ∈ 𝐼 ↦ (𝐹‘((𝑋‘𝑦) + (𝑌‘𝑦)))))
31		fvexd 6907	. . 3 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝐹‘(𝑋‘𝑦)) ∈ V)
32		fvexd 6907	. . 3 ⊢ (((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑦 ∈ 𝐼) → (𝐹‘(𝑌‘𝑦)) ∈ V)
33		fcompt 7131	. . . 4 ⊢ ((𝐹:𝐵⟶(Base‘𝑁) ∧ 𝑋:𝐼⟶𝐵) → (𝐹 ∘ 𝑋) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑋‘𝑦))))
34	27, 3, 33	syl2anc 585	. . 3 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝐹 ∘ 𝑋) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑋‘𝑦))))
35		fcompt 7131	. . . 4 ⊢ ((𝐹:𝐵⟶(Base‘𝑁) ∧ 𝑌:𝐼⟶𝐵) → (𝐹 ∘ 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑌‘𝑦))))
36	27, 6, 35	syl2anc 585	. . 3 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝐹 ∘ 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝐹‘(𝑌‘𝑦))))
37	21, 31, 32, 34, 36	offval2 7690	. 2 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → ((𝐹 ∘ 𝑋) ∘_f ⨣ (𝐹 ∘ 𝑌)) = (𝑦 ∈ 𝐼 ↦ ((𝐹‘(𝑋‘𝑦)) ⨣ (𝐹‘(𝑌‘𝑦)))))
38	13, 30, 37	3eqtr4d 2783	1 ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑_m 𝐼)) → (𝐹 ∘ (𝑋 ∘_f + 𝑌)) = ((𝐹 ∘ 𝑋) ∘_f ⨣ (𝐹 ∘ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 Vcvv 3475 ↦ cmpt 5232 ∘ ccom 5681 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ∘_f cof 7668 ↑_m cmap 8820 Basecbs 17144 +_gcplusg 17197 Mndcmnd 18625 MndHom cmhm 18669

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-of 7670 df-1st 7975 df-2nd 7976 df-map 8822 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-mhm 18671

This theorem is referenced by: mhmcoaddmpl 41171 mendring 41982

W3C validator