frmdup3lem

	Ref	Expression
Hypotheses	frmdup3.m	$⊢ M = freeMnd (I)$
	frmdup3.b	$⊢ B = {Base}_{G}$
	frmdup3.u	$⊢ U = {var}_{FMnd} (I)$
Assertion	frmdup3lem	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to F = (x \in Word I ⟼ \sum_{G} (A \circ x))$

Proof

Step	Hyp	Ref	Expression
1		frmdup3.m	$⊢ M = freeMnd (I)$
2		frmdup3.b	$⊢ B = {Base}_{G}$
3		frmdup3.u	$⊢ U = {var}_{FMnd} (I)$
4		eqid	$⊢ {Base}_{M} = {Base}_{M}$
5	4 2	mhmf	$⊢ F \in (M MndHom G) \to F : {Base}_{M} ⟶ B$
6	5	ad2antrl	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to F : {Base}_{M} ⟶ B$
7	1 4	frmdbas	$⊢ I \in V \to {Base}_{M} = Word I$
8	7	3ad2ant2	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to {Base}_{M} = Word I$
9	8	adantr	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to {Base}_{M} = Word I$
10	9	feq2d	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to (F : {Base}_{M} ⟶ B \leftrightarrow F : Word I ⟶ B)$
11	6 10	mpbid	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to F : Word I ⟶ B$
12	11	feqmptd	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to F = (x \in Word I ⟼ F (x))$
13		simplrl	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to F \in (M MndHom G)$
14		simpr	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to x \in Word I$
15	3	vrmdf	$⊢ I \in V \to U : I ⟶ Word I$
16	15	3ad2ant2	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to U : I ⟶ Word I$
17	8	feq3d	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to (U : I ⟶ {Base}_{M} \leftrightarrow U : I ⟶ Word I)$
18	16 17	mpbird	$⊢ (G \in Mnd \land I \in V \land A : I ⟶ B) \to U : I ⟶ {Base}_{M}$
19	18	ad2antrr	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to U : I ⟶ {Base}_{M}$
20		wrdco	$⊢ (x \in Word I \land U : I ⟶ {Base}_{M}) \to U \circ x \in Word {Base}_{M}$
21	14 19 20	syl2anc	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to U \circ x \in Word {Base}_{M}$
22	4	gsumwmhm	$⊢ (F \in (M MndHom G) \land U \circ x \in Word {Base}_{M}) \to F (\sum_{M} (U \circ x)) = \sum_{G} (F \circ (U \circ x))$
23	13 21 22	syl2anc	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to F (\sum_{M} (U \circ x)) = \sum_{G} (F \circ (U \circ x))$
24		simpll2	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to I \in V$
25	1 3	frmdgsum	$⊢ (I \in V \land x \in Word I) \to \sum_{M} (U \circ x) = x$
26	24 14 25	syl2anc	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to \sum_{M} (U \circ x) = x$
27	26	fveq2d	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to F (\sum_{M} (U \circ x)) = F (x)$
28		coass	$⊢ (F \circ U) \circ x = F \circ (U \circ x)$
29		simplrr	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to F \circ U = A$
30	29	coeq1d	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to (F \circ U) \circ x = A \circ x$
31	28 30	eqtr3id	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to F \circ (U \circ x) = A \circ x$
32	31	oveq2d	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to \sum_{G} (F \circ (U \circ x)) = \sum_{G} (A \circ x)$
33	23 27 32	3eqtr3d	$⊢ (((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \land x \in Word I) \to F (x) = \sum_{G} (A \circ x)$
34	33	mpteq2dva	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to (x \in Word I ⟼ F (x)) = (x \in Word I ⟼ \sum_{G} (A \circ x))$
35	12 34	eqtrd	$⊢ ((G \in Mnd \land I \in V \land A : I ⟶ B) \land (F \in (M MndHom G) \land F \circ U = A)) \to F = (x \in Word I ⟼ \sum_{G} (A \circ x))$

Metamath Proof Explorer

Theorem frmdup3lem

Proof