Metamath Proof Explorer


Theorem frmdup3lem

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

Ref Expression
Hypotheses frmdup3.m 𝑀 = ( freeMnd ‘ 𝐼 )
frmdup3.b 𝐵 = ( Base ‘ 𝐺 )
frmdup3.u 𝑈 = ( varFMnd𝐼 )
Assertion frmdup3lem ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → 𝐹 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 frmdup3.m 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdup3.b 𝐵 = ( Base ‘ 𝐺 )
3 frmdup3.u 𝑈 = ( varFMnd𝐼 )
4 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5 4 2 mhmf ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ 𝐵 )
6 5 ad2antrl ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ 𝐵 )
7 1 4 frmdbas ( 𝐼𝑉 → ( Base ‘ 𝑀 ) = Word 𝐼 )
8 7 3ad2ant2 ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
9 8 adantr ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → ( Base ‘ 𝑀 ) = Word 𝐼 )
10 9 feq2d ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → ( 𝐹 : ( Base ‘ 𝑀 ) ⟶ 𝐵𝐹 : Word 𝐼𝐵 ) )
11 6 10 mpbid ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → 𝐹 : Word 𝐼𝐵 )
12 11 feqmptd ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → 𝐹 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐹𝑥 ) ) )
13 simplrl ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) )
14 simpr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → 𝑥 ∈ Word 𝐼 )
15 3 vrmdf ( 𝐼𝑉𝑈 : 𝐼 ⟶ Word 𝐼 )
16 15 3ad2ant2 ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) → 𝑈 : 𝐼 ⟶ Word 𝐼 )
17 8 feq3d ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) → ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ↔ 𝑈 : 𝐼 ⟶ Word 𝐼 ) )
18 16 17 mpbird ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) )
19 18 ad2antrr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) )
20 wrdco ( ( 𝑥 ∈ Word 𝐼𝑈 : 𝐼 ⟶ ( Base ‘ 𝑀 ) ) → ( 𝑈𝑥 ) ∈ Word ( Base ‘ 𝑀 ) )
21 14 19 20 syl2anc ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝑈𝑥 ) ∈ Word ( Base ‘ 𝑀 ) )
22 4 gsumwmhm ( ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝑈𝑥 ) ∈ Word ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑀 Σg ( 𝑈𝑥 ) ) ) = ( 𝐺 Σg ( 𝐹 ∘ ( 𝑈𝑥 ) ) ) )
23 13 21 22 syl2anc ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐹 ‘ ( 𝑀 Σg ( 𝑈𝑥 ) ) ) = ( 𝐺 Σg ( 𝐹 ∘ ( 𝑈𝑥 ) ) ) )
24 simpll2 ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → 𝐼𝑉 )
25 1 3 frmdgsum ( ( 𝐼𝑉𝑥 ∈ Word 𝐼 ) → ( 𝑀 Σg ( 𝑈𝑥 ) ) = 𝑥 )
26 24 14 25 syl2anc ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝑀 Σg ( 𝑈𝑥 ) ) = 𝑥 )
27 26 fveq2d ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐹 ‘ ( 𝑀 Σg ( 𝑈𝑥 ) ) ) = ( 𝐹𝑥 ) )
28 coass ( ( 𝐹𝑈 ) ∘ 𝑥 ) = ( 𝐹 ∘ ( 𝑈𝑥 ) )
29 simplrr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐹𝑈 ) = 𝐴 )
30 29 coeq1d ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( ( 𝐹𝑈 ) ∘ 𝑥 ) = ( 𝐴𝑥 ) )
31 28 30 eqtr3id ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐹 ∘ ( 𝑈𝑥 ) ) = ( 𝐴𝑥 ) )
32 31 oveq2d ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐺 Σg ( 𝐹 ∘ ( 𝑈𝑥 ) ) ) = ( 𝐺 Σg ( 𝐴𝑥 ) ) )
33 23 27 32 3eqtr3d ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) ∧ 𝑥 ∈ Word 𝐼 ) → ( 𝐹𝑥 ) = ( 𝐺 Σg ( 𝐴𝑥 ) ) )
34 33 mpteq2dva ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴𝑥 ) ) ) )
35 12 34 eqtrd ( ( ( 𝐺 ∈ Mnd ∧ 𝐼𝑉𝐴 : 𝐼𝐵 ) ∧ ( 𝐹 ∈ ( 𝑀 MndHom 𝐺 ) ∧ ( 𝐹𝑈 ) = 𝐴 ) ) → 𝐹 = ( 𝑥 ∈ Word 𝐼 ↦ ( 𝐺 Σg ( 𝐴𝑥 ) ) ) )