Metamath Proof Explorer


Theorem frmdup2

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

Ref Expression
Hypotheses frmdup.m M = freeMnd I
frmdup.b B = Base G
frmdup.e E = x Word I G A x
frmdup.g φ G Mnd
frmdup.i φ I X
frmdup.a φ A : I B
frmdup2.u U = var FMnd I
frmdup2.y φ Y I
Assertion frmdup2 φ E U Y = A Y

Proof

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