Metamath Proof Explorer

Theorem ghmquskerco

Description: In the case of theorem ghmqusker , the composition of the natural homomorphism L with the constructed homomorphism J equals the original homomorphism F . One says that F factors through Q . (Proposed by Saveliy Skresanov, 15-Feb-2025.) (Contributed by Thierry Arnoux, 15-Feb-2025)

Ref Expression
Hypotheses ghmqusker.1 
|- .0. = ( 0g ` H )
ghmqusker.f 
|- ( ph -> F e. ( G GrpHom H ) )
ghmqusker.k 
|- K = ( `' F " { .0. } )
ghmqusker.q 
|- Q = ( G /s ( G ~QG K ) )
ghmqusker.j 
|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
ghmquskerco.b 
|- B = ( Base ` G )
ghmquskerco.l 
|- L = ( x e. B |-> [ x ] ( G ~QG K ) )
Assertion ghmquskerco 
|- ( ph -> F = ( J o. L ) )

Proof

Step Hyp Ref Expression
1 ghmqusker.1 
 |-  .0. = ( 0g ` H )
2 ghmqusker.f 
 |-  ( ph -> F e. ( G GrpHom H ) )
3 ghmqusker.k 
 |-  K = ( `' F " { .0. } )
4 ghmqusker.q 
 |-  Q = ( G /s ( G ~QG K ) )
5 ghmqusker.j 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
6 ghmquskerco.b 
 |-  B = ( Base ` G )
7 ghmquskerco.l 
 |-  L = ( x e. B |-> [ x ] ( G ~QG K ) )
8 eqid 
 |-  ( Base ` H ) = ( Base ` H )
9 6 8 ghmf 
 |-  ( F e. ( G GrpHom H ) -> F : B --> ( Base ` H ) )
10 2 9 syl 
 |-  ( ph -> F : B --> ( Base ` H ) )
11 10 ffnd 
 |-  ( ph -> F Fn B )
12 2 adantr 
 |-  ( ( ph /\ x e. B ) -> F e. ( G GrpHom H ) )
13 12 imaexd 
 |-  ( ( ph /\ x e. B ) -> ( F " [ x ] ( G ~QG K ) ) e. _V )
14 13 uniexd 
 |-  ( ( ph /\ x e. B ) -> U. ( F " [ x ] ( G ~QG K ) ) e. _V )
15 14 ralrimiva 
 |-  ( ph -> A. x e. B U. ( F " [ x ] ( G ~QG K ) ) e. _V )
16 eqid 
 |-  ( x e. B |-> U. ( F " [ x ] ( G ~QG K ) ) ) = ( x e. B |-> U. ( F " [ x ] ( G ~QG K ) ) )
17 16 fnmpt 
 |-  ( A. x e. B U. ( F " [ x ] ( G ~QG K ) ) e. _V -> ( x e. B |-> U. ( F " [ x ] ( G ~QG K ) ) ) Fn B )
18 15 17 syl 
 |-  ( ph -> ( x e. B |-> U. ( F " [ x ] ( G ~QG K ) ) ) Fn B )
19 ovex 
 |-  ( G ~QG K ) e. _V
20 19 ecelqsi 
 |-  ( x e. B -> [ x ] ( G ~QG K ) e. ( B /. ( G ~QG K ) ) )
21 20 adantl 
 |-  ( ( ph /\ x e. B ) -> [ x ] ( G ~QG K ) e. ( B /. ( G ~QG K ) ) )
22 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG K ) ) )
23 6 a1i 
 |-  ( ph -> B = ( Base ` G ) )
24 ovexd 
 |-  ( ph -> ( G ~QG K ) e. _V )
25 reldmghm 
 |-  Rel dom GrpHom
26 25 ovrcl 
 |-  ( F e. ( G GrpHom H ) -> ( G e. _V /\ H e. _V ) )
27 26 simpld 
 |-  ( F e. ( G GrpHom H ) -> G e. _V )
28 2 27 syl 
 |-  ( ph -> G e. _V )
29 22 23 24 28 qusbas 
 |-  ( ph -> ( B /. ( G ~QG K ) ) = ( Base ` Q ) )
30 29 adantr 
 |-  ( ( ph /\ x e. B ) -> ( B /. ( G ~QG K ) ) = ( Base ` Q ) )
31 21 30 eleqtrd 
 |-  ( ( ph /\ x e. B ) -> [ x ] ( G ~QG K ) e. ( Base ` Q ) )
32 7 a1i 
 |-  ( ph -> L = ( x e. B |-> [ x ] ( G ~QG K ) ) )
33 5 a1i 
 |-  ( ph -> J = ( q e. ( Base ` Q ) |-> U. ( F " q ) ) )
34 imaeq2 
 |-  ( q = [ x ] ( G ~QG K ) -> ( F " q ) = ( F " [ x ] ( G ~QG K ) ) )
35 34 unieqd 
 |-  ( q = [ x ] ( G ~QG K ) -> U. ( F " q ) = U. ( F " [ x ] ( G ~QG K ) ) )
36 31 32 33 35 fmptco 
 |-  ( ph -> ( J o. L ) = ( x e. B |-> U. ( F " [ x ] ( G ~QG K ) ) ) )
37 36 fneq1d 
 |-  ( ph -> ( ( J o. L ) Fn B <-> ( x e. B |-> U. ( F " [ x ] ( G ~QG K ) ) ) Fn B ) )
38 18 37 mpbird 
 |-  ( ph -> ( J o. L ) Fn B )
39 ecexg 
 |-  ( ( G ~QG K ) e. _V -> [ x ] ( G ~QG K ) e. _V )
40 19 39 ax-mp 
 |-  [ x ] ( G ~QG K ) e. _V
41 40 7 fnmpti 
 |-  L Fn B
42 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
43 fvco2 
 |-  ( ( L Fn B /\ x e. B ) -> ( ( J o. L ) ` x ) = ( J ` ( L ` x ) ) )
44 41 42 43 sylancr 
 |-  ( ( ph /\ x e. B ) -> ( ( J o. L ) ` x ) = ( J ` ( L ` x ) ) )
45 40 a1i 
 |-  ( ( ph /\ x e. B ) -> [ x ] ( G ~QG K ) e. _V )
46 32 45 fvmpt2d 
 |-  ( ( ph /\ x e. B ) -> ( L ` x ) = [ x ] ( G ~QG K ) )
47 46 fveq2d 
 |-  ( ( ph /\ x e. B ) -> ( J ` ( L ` x ) ) = ( J ` [ x ] ( G ~QG K ) ) )
48 42 6 eleqtrdi 
 |-  ( ( ph /\ x e. B ) -> x e. ( Base ` G ) )
49 1 12 3 4 5 48 ghmquskerlem1 
 |-  ( ( ph /\ x e. B ) -> ( J ` [ x ] ( G ~QG K ) ) = ( F ` x ) )
50 44 47 49 3eqtrrd 
 |-  ( ( ph /\ x e. B ) -> ( F ` x ) = ( ( J o. L ) ` x ) )
51 11 38 50 eqfnfvd 
 |-  ( ph -> F = ( J o. L ) )