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 syl5eqr ⊢ ( ( ( ( 𝐺 ∈ 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 ( 𝐴 ∘ 𝑥 ) ) ) )