This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusker

Description: The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypotheses qusker.b 
|- V = ( Base ` M )
qusker.f 
|- F = ( x e. V |-> [ x ] ( M ~QG G ) )
qusker.n 
|- N = ( M /s ( M ~QG G ) )
qusker.1 
|- .0. = ( 0g ` N )
Assertion qusker 
|- ( G e. ( NrmSGrp ` M ) -> ( `' F " { .0. } ) = G )

Proof

Step Hyp Ref Expression
1 qusker.b 
 |-  V = ( Base ` M )
2 qusker.f 
 |-  F = ( x e. V |-> [ x ] ( M ~QG G ) )
3 qusker.n 
 |-  N = ( M /s ( M ~QG G ) )
4 qusker.1 
 |-  .0. = ( 0g ` N )
5 3 a1i 
 |-  ( G e. ( NrmSGrp ` M ) -> N = ( M /s ( M ~QG G ) ) )
6 1 a1i 
 |-  ( G e. ( NrmSGrp ` M ) -> V = ( Base ` M ) )
7 ovex 
 |-  ( M ~QG G ) e. _V
8 7 a1i 
 |-  ( G e. ( NrmSGrp ` M ) -> ( M ~QG G ) e. _V )
9 nsgsubg 
 |-  ( G e. ( NrmSGrp ` M ) -> G e. ( SubGrp ` M ) )
10 subgrcl 
 |-  ( G e. ( SubGrp ` M ) -> M e. Grp )
11 9 10 syl 
 |-  ( G e. ( NrmSGrp ` M ) -> M e. Grp )
12 5 6 2 8 11 quslem 
 |-  ( G e. ( NrmSGrp ` M ) -> F : V -onto-> ( V /. ( M ~QG G ) ) )
13 fofn 
 |-  ( F : V -onto-> ( V /. ( M ~QG G ) ) -> F Fn V )
14 fniniseg2 
 |-  ( F Fn V -> ( `' F " { .0. } ) = { y e. V | ( F ` y ) = .0. } )
15 12 13 14 3syl 
 |-  ( G e. ( NrmSGrp ` M ) -> ( `' F " { .0. } ) = { y e. V | ( F ` y ) = .0. } )
16 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
17 3 16 qus0 
 |-  ( G e. ( NrmSGrp ` M ) -> [ ( 0g ` M ) ] ( M ~QG G ) = ( 0g ` N ) )
18 4 17 eqtr4id 
 |-  ( G e. ( NrmSGrp ` M ) -> .0. = [ ( 0g ` M ) ] ( M ~QG G ) )
19 eceq1 
 |-  ( x = y -> [ x ] ( M ~QG G ) = [ y ] ( M ~QG G ) )
20 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ y ] ( M ~QG G ) e. _V )
21 7 20 ax-mp 
 |-  [ y ] ( M ~QG G ) e. _V
22 19 2 21 fvmpt 
 |-  ( y e. V -> ( F ` y ) = [ y ] ( M ~QG G ) )
23 18 22 eqeqan12d 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( .0. = ( F ` y ) <-> [ ( 0g ` M ) ] ( M ~QG G ) = [ y ] ( M ~QG G ) ) )
24 eqcom 
 |-  ( .0. = ( F ` y ) <-> ( F ` y ) = .0. )
25 24 a1i 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( .0. = ( F ` y ) <-> ( F ` y ) = .0. ) )
26 simpl 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> G e. ( NrmSGrp ` M ) )
27 simpr 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> y e. V )
28 1 16 grpidcl 
 |-  ( M e. Grp -> ( 0g ` M ) e. V )
29 26 11 28 3syl 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( 0g ` M ) e. V )
30 1 subgss 
 |-  ( G e. ( SubGrp ` M ) -> G C_ V )
31 9 30 syl 
 |-  ( G e. ( NrmSGrp ` M ) -> G C_ V )
32 eqid 
 |-  ( invg ` M ) = ( invg ` M )
33 eqid 
 |-  ( +g ` M ) = ( +g ` M )
34 eqid 
 |-  ( M ~QG G ) = ( M ~QG G )
35 1 32 33 34 eqgval 
 |-  ( ( M e. Grp /\ G C_ V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) )
36 11 31 35 syl2anc 
 |-  ( G e. ( NrmSGrp ` M ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) )
37 36 adantr 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) ) )
38 df-3an 
 |-  ( ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) <-> ( ( ( 0g ` M ) e. V /\ y e. V ) /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) )
39 38 biancomi 
 |-  ( ( ( 0g ` M ) e. V /\ y e. V /\ ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) <-> ( ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G /\ ( ( 0g ` M ) e. V /\ y e. V ) ) )
40 37 39 bitrdi 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G /\ ( ( 0g ` M ) e. V /\ y e. V ) ) ) )
41 40 rbaibd 
 |-  ( ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) /\ ( ( 0g ` M ) e. V /\ y e. V ) ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) )
42 26 27 29 27 41 syl22anc 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G ) )
43 1 34 eqger 
 |-  ( G e. ( SubGrp ` M ) -> ( M ~QG G ) Er V )
44 9 43 syl 
 |-  ( G e. ( NrmSGrp ` M ) -> ( M ~QG G ) Er V )
45 44 adantr 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( M ~QG G ) Er V )
46 45 27 erth2 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( M ~QG G ) y <-> [ ( 0g ` M ) ] ( M ~QG G ) = [ y ] ( M ~QG G ) ) )
47 16 32 grpinvid 
 |-  ( M e. Grp -> ( ( invg ` M ) ` ( 0g ` M ) ) = ( 0g ` M ) )
48 26 11 47 3syl 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( invg ` M ) ` ( 0g ` M ) ) = ( 0g ` M ) )
49 48 oveq1d 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) = ( ( 0g ` M ) ( +g ` M ) y ) )
50 1 33 16 grplid 
 |-  ( ( M e. Grp /\ y e. V ) -> ( ( 0g ` M ) ( +g ` M ) y ) = y )
51 11 50 sylan 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( 0g ` M ) ( +g ` M ) y ) = y )
52 49 51 eqtrd 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) = y )
53 52 eleq1d 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( ( ( invg ` M ) ` ( 0g ` M ) ) ( +g ` M ) y ) e. G <-> y e. G ) )
54 42 46 53 3bitr3d 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( [ ( 0g ` M ) ] ( M ~QG G ) = [ y ] ( M ~QG G ) <-> y e. G ) )
55 23 25 54 3bitr3d 
 |-  ( ( G e. ( NrmSGrp ` M ) /\ y e. V ) -> ( ( F ` y ) = .0. <-> y e. G ) )
56 55 rabbidva 
 |-  ( G e. ( NrmSGrp ` M ) -> { y e. V | ( F ` y ) = .0. } = { y e. V | y e. G } )
57 dfss7 
 |-  ( G C_ V <-> { y e. V | y e. G } = G )
58 31 57 sylib 
 |-  ( G e. ( NrmSGrp ` M ) -> { y e. V | y e. G } = G )
59 15 56 58 3eqtrd 
 |-  ( G e. ( NrmSGrp ` M ) -> ( `' F " { .0. } ) = G )