Metamath Proof Explorer

Theorem frgpup3

Description: Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup3.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
frgpup3.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
frgpup3.u ⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
Assertion frgpup3 ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ∃! 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ( 𝑚 ∘ 𝑈 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 frgpup3.g ⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgpup3.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
3 frgpup3.u ⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
4 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
5 eqid ⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
6 simp1 ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐻 ∈ Grp )
7 simp2 ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐼 ∈ 𝑉 )
8 simp3 ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
9 eqid ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
10 eqid ⊢ ( ~FG ‘ 𝐼 ) = ( ~FG ‘ 𝐼 )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 eqid ⊢ ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ )
13 2 4 5 6 7 8 9 10 1 11 12 frgpup1 ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∈ ( 𝐺 GrpHom 𝐻 ) )
14 6 adantr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐻 ∈ Grp )
15 7 adantr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
16 8 adantr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
17 simpr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
18 2 4 5 14 15 16 9 10 1 11 12 3 17 frgpup2 ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑘 ∈ 𝐼 ) → ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ‘ ( 𝑈 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
19 18 mpteq2dva ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝑘 ∈ 𝐼 ↦ ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ‘ ( 𝑈 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) )
20 11 2 ghmf ⊢ ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∈ ( 𝐺 GrpHom 𝐻 ) → ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) : ( Base ‘ 𝐺 ) ⟶ 𝐵 )
21 13 20 syl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) : ( Base ‘ 𝐺 ) ⟶ 𝐵 )
22 10 3 1 11 vrgpf ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
23 7 22 syl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
24 fcompt ⊢ ( ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) : ( Base ‘ 𝐺 ) ⟶ 𝐵 ∧ 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐺 ) ) → ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∘ 𝑈 ) = ( 𝑘 ∈ 𝐼 ↦ ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ‘ ( 𝑈 ‘ 𝑘 ) ) ) )
25 21 23 24 syl2anc ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∘ 𝑈 ) = ( 𝑘 ∈ 𝐼 ↦ ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ‘ ( 𝑈 ‘ 𝑘 ) ) ) )
26 8 feqmptd ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑘 ) ) )
27 19 25 26 3eqtr4d ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∘ 𝑈 ) = 𝐹 )
28 6 adantr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐹 ) ) → 𝐻 ∈ Grp )
29 7 adantr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐹 ) ) → 𝐼 ∈ 𝑉 )
30 8 adantr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐹 ) ) → 𝐹 : 𝐼 ⟶ 𝐵 )
31 simprl ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐹 ) ) → 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) )
32 simprr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐹 ) ) → ( 𝑚 ∘ 𝑈 ) = 𝐹 )
33 2 4 5 28 29 30 9 10 1 11 12 3 31 32 frgpup3lem ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑚 ∘ 𝑈 ) = 𝐹 ) ) → 𝑚 = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) )
34 33 expr ⊢ ( ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐹 → 𝑚 = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ) )
35 34 ralrimiva ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ∀ 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐹 → 𝑚 = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ) )
36 coeq1 ⊢ ( 𝑚 = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) → ( 𝑚 ∘ 𝑈 ) = ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∘ 𝑈 ) )
37 36 eqeq1d ⊢ ( 𝑚 = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐹 ↔ ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∘ 𝑈 ) = 𝐹 ) )
38 37 eqreu ⊢ ( ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ∘ 𝑈 ) = 𝐹 ∧ ∀ 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐹 → 𝑚 = ran ( 𝑔 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) ↦ ⟨ [ 𝑔 ] ( ~FG ‘ 𝐼 ) , ( 𝐻 Σg ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) ∘ 𝑔 ) ) ⟩ ) ) ) → ∃! 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ( 𝑚 ∘ 𝑈 ) = 𝐹 )
39 13 27 35 38 syl3anc ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ∃! 𝑚 ∈ ( 𝐺 GrpHom 𝐻 ) ( 𝑚 ∘ 𝑈 ) = 𝐹 )