frmdup2

Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015)

Step	Hyp	Ref	Expression
1		frmdup.m	$⊢ M = freeMnd (I)$
2		frmdup.b	$⊢ B = {Base}_{G}$
3		frmdup.e	$⊢ E = (x \in Word I ⟼ \sum_{G} (A \circ x))$
4		frmdup.g	$⊢ φ \to G \in Mnd$
5		frmdup.i	$⊢ φ \to I \in X$
6		frmdup.a	$⊢ φ \to A : I ⟶ B$
7		frmdup2.u	$⊢ U = {var}_{FMnd} (I)$
8		frmdup2.y	$⊢ φ \to Y \in I$
9	7	vrmdval	$⊢ (I \in X \land Y \in I) \to U (Y) = ⟨“ Y ”⟩$
10	5 8 9	syl2anc	$⊢ φ \to U (Y) = ⟨“ Y ”⟩$
11	10	fveq2d	$⊢ φ \to E (U (Y)) = E (⟨“ Y ”⟩)$
12	8	s1cld	$⊢ φ \to ⟨“ Y ”⟩ \in Word I$
13		coeq2	$⊢ x = ⟨“ Y ”⟩ \to A \circ x = A \circ ⟨“ Y ”⟩$
14	13	oveq2d	$⊢ x = ⟨“ Y ”⟩ \to \sum_{G} (A \circ x) = \sum_{G} (A \circ ⟨“ Y ”⟩)$
15		ovex	$⊢ \sum_{G} (A \circ x) \in V$
16	14 3 15	fvmpt3i	$⊢ ⟨“ Y ”⟩ \in Word I \to E (⟨“ Y ”⟩) = \sum_{G} (A \circ ⟨“ Y ”⟩)$
17	12 16	syl	$⊢ φ \to E (⟨“ Y ”⟩) = \sum_{G} (A \circ ⟨“ Y ”⟩)$
18		s1co	$⊢ (Y \in I \land A : I ⟶ B) \to A \circ ⟨“ Y ”⟩ = ⟨“ A (Y) ”⟩$
19	8 6 18	syl2anc	$⊢ φ \to A \circ ⟨“ Y ”⟩ = ⟨“ A (Y) ”⟩$
20	19	oveq2d	$⊢ φ \to \sum_{G} (A \circ ⟨“ Y ”⟩) = \sum_{G} ⟨“ A (Y) ”⟩$
21	6 8	ffvelrnd	$⊢ φ \to A (Y) \in B$
22	2	gsumws1	$⊢ A (Y) \in B \to \sum_{G} ⟨“ A (Y) ”⟩ = A (Y)$
23	21 22	syl	$⊢ φ \to \sum_{G} ⟨“ A (Y) ”⟩ = A (Y)$
24	17 20 23	3eqtrd	$⊢ φ \to E (⟨“ Y ”⟩) = A (Y)$
25	11 24	eqtrd	$⊢ φ \to E (U (Y)) = A (Y)$

Metamath Proof Explorer