Metamath Proof Explorer


Theorem frmdup3lem

Description: Lemma for frmdup3 . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses frmdup3.m M = freeMnd I
frmdup3.b B = Base G
frmdup3.u U = var FMnd I
Assertion frmdup3lem G Mnd I V A : I B F M MndHom G F U = A F = x Word I G A 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 M MndHom G F : Base M B
6 5 ad2antrl G Mnd I V A : I B F M MndHom G F U = A F : Base M B
7 1 4 frmdbas I V Base M = Word I
8 7 3ad2ant2 G Mnd I V A : I B Base M = Word I
9 8 adantr G Mnd I V A : I B F M MndHom G F U = A Base M = Word I
10 9 feq2d G Mnd I V A : I B F M MndHom G F U = A F : Base M B F : Word I B
11 6 10 mpbid G Mnd I V A : I B F M MndHom G F U = A F : Word I B
12 11 feqmptd G Mnd I V A : I B F M MndHom G F U = A F = x Word I F x
13 simplrl G Mnd I V A : I B F M MndHom G F U = A x Word I F M MndHom G
14 simpr G Mnd I V A : I B F M MndHom G F U = A x Word I x Word I
15 3 vrmdf I V U : I Word I
16 15 3ad2ant2 G Mnd I V A : I B U : I Word I
17 8 feq3d G Mnd I V A : I B U : I Base M U : I Word I
18 16 17 mpbird G Mnd I V A : I B U : I Base M
19 18 ad2antrr G Mnd I V A : I B F M MndHom G F U = A x Word I U : I Base M
20 wrdco x Word I U : I Base M U x Word Base M
21 14 19 20 syl2anc G Mnd I V A : I B F M MndHom G F U = A x Word I U x Word Base M
22 4 gsumwmhm F M MndHom G U x Word Base M F M U x = G F U x
23 13 21 22 syl2anc G Mnd I V A : I B F M MndHom G F U = A x Word I F M U x = G F U x
24 simpll2 G Mnd I V A : I B F M MndHom G F U = A x Word I I V
25 1 3 frmdgsum I V x Word I M U x = x
26 24 14 25 syl2anc G Mnd I V A : I B F M MndHom G F U = A x Word I M U x = x
27 26 fveq2d G Mnd I V A : I B F M MndHom G F U = A x Word I F M U x = F x
28 coass F U x = F U x
29 simplrr G Mnd I V A : I B F M MndHom G F U = A x Word I F U = A
30 29 coeq1d G Mnd I V A : I B F M MndHom G F U = A x Word I F U x = A x
31 28 30 eqtr3id G Mnd I V A : I B F M MndHom G F U = A x Word I F U x = A x
32 31 oveq2d G Mnd I V A : I B F M MndHom G F U = A x Word I G F U x = G A x
33 23 27 32 3eqtr3d G Mnd I V A : I B F M MndHom G F U = A x Word I F x = G A x
34 33 mpteq2dva G Mnd I V A : I B F M MndHom G F U = A x Word I F x = x Word I G A x
35 12 34 eqtrd G Mnd I V A : I B F M MndHom G F U = A F = x Word I G A x