Metamath Proof Explorer

Theorem nsgmgclem

Description: Lemma for nsgmgc . (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses nsgmgclem.b 
|- B = ( Base ` G )
nsgmgclem.q 
|- Q = ( G /s ( G ~QG N ) )
nsgmgclem.p 
|- .(+) = ( LSSum ` G )
nsgmgclem.n 
|- ( ph -> N e. ( NrmSGrp ` G ) )
nsgmgclem.f 
|- ( ph -> F e. ( SubGrp ` Q ) )
Assertion nsgmgclem 
|- ( ph -> { a e. B | ( { a } .(+) N ) e. F } e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 nsgmgclem.b 
 |-  B = ( Base ` G )
2 nsgmgclem.q 
 |-  Q = ( G /s ( G ~QG N ) )
3 nsgmgclem.p 
 |-  .(+) = ( LSSum ` G )
4 nsgmgclem.n 
 |-  ( ph -> N e. ( NrmSGrp ` G ) )
5 nsgmgclem.f 
 |-  ( ph -> F e. ( SubGrp ` Q ) )
6 eqidd 
 |-  ( ph -> ( G |`s { a e. B | ( { a } .(+) N ) e. F } ) = ( G |`s { a e. B | ( { a } .(+) N ) e. F } ) )
7 eqidd 
 |-  ( ph -> ( 0g ` G ) = ( 0g ` G ) )
8 eqidd 
 |-  ( ph -> ( +g ` G ) = ( +g ` G ) )
9 ssrab2 
 |-  { a e. B | ( { a } .(+) N ) e. F } C_ B
10 9 a1i 
 |-  ( ph -> { a e. B | ( { a } .(+) N ) e. F } C_ B )
11 10 1 sseqtrdi 
 |-  ( ph -> { a e. B | ( { a } .(+) N ) e. F } C_ ( Base ` G ) )
12 sneq 
 |-  ( a = ( 0g ` G ) -> { a } = { ( 0g ` G ) } )
13 12 oveq1d 
 |-  ( a = ( 0g ` G ) -> ( { a } .(+) N ) = ( { ( 0g ` G ) } .(+) N ) )
14 13 eleq1d 
 |-  ( a = ( 0g ` G ) -> ( ( { a } .(+) N ) e. F <-> ( { ( 0g ` G ) } .(+) N ) e. F ) )
15 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
16 4 15 syl 
 |-  ( ph -> N e. ( SubGrp ` G ) )
17 subgrcl 
 |-  ( N e. ( SubGrp ` G ) -> G e. Grp )
18 16 17 syl 
 |-  ( ph -> G e. Grp )
19 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
20 1 19 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
21 18 20 syl 
 |-  ( ph -> ( 0g ` G ) e. B )
22 19 3 lsm02 
 |-  ( N e. ( SubGrp ` G ) -> ( { ( 0g ` G ) } .(+) N ) = N )
23 16 22 syl 
 |-  ( ph -> ( { ( 0g ` G ) } .(+) N ) = N )
24 2 nsgqus0 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ F e. ( SubGrp ` Q ) ) -> N e. F )
25 4 5 24 syl2anc 
 |-  ( ph -> N e. F )
26 23 25 eqeltrd 
 |-  ( ph -> ( { ( 0g ` G ) } .(+) N ) e. F )
27 14 21 26 elrabd 
 |-  ( ph -> ( 0g ` G ) e. { a e. B | ( { a } .(+) N ) e. F } )
28 sneq 
 |-  ( a = ( x ( +g ` G ) y ) -> { a } = { ( x ( +g ` G ) y ) } )
29 28 oveq1d 
 |-  ( a = ( x ( +g ` G ) y ) -> ( { a } .(+) N ) = ( { ( x ( +g ` G ) y ) } .(+) N ) )
30 29 eleq1d 
 |-  ( a = ( x ( +g ` G ) y ) -> ( ( { a } .(+) N ) e. F <-> ( { ( x ( +g ` G ) y ) } .(+) N ) e. F ) )
31 18 ad2antrr 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> G e. Grp )
32 elrabi 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. F } -> x e. B )
33 32 ad2antlr 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> x e. B )
34 elrabi 
 |-  ( y e. { a e. B | ( { a } .(+) N ) e. F } -> y e. B )
35 34 adantl 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> y e. B )
36 eqid 
 |-  ( +g ` G ) = ( +g ` G )
37 1 36 grpcl 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
38 31 33 35 37 syl3anc 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( x ( +g ` G ) y ) e. B )
39 16 ad2antrr 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> N e. ( SubGrp ` G ) )
40 1 3 39 38 quslsm 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> [ ( x ( +g ` G ) y ) ] ( G ~QG N ) = ( { ( x ( +g ` G ) y ) } .(+) N ) )
41 4 ad2antrr 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> N e. ( NrmSGrp ` G ) )
42 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
43 2 1 36 42 qusadd 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ x e. B /\ y e. B ) -> ( [ x ] ( G ~QG N ) ( +g ` Q ) [ y ] ( G ~QG N ) ) = [ ( x ( +g ` G ) y ) ] ( G ~QG N ) )
44 41 33 35 43 syl3anc 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( [ x ] ( G ~QG N ) ( +g ` Q ) [ y ] ( G ~QG N ) ) = [ ( x ( +g ` G ) y ) ] ( G ~QG N ) )
45 5 ad2antrr 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> F e. ( SubGrp ` Q ) )
46 1 3 39 33 quslsm 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> [ x ] ( G ~QG N ) = ( { x } .(+) N ) )
47 sneq 
 |-  ( a = x -> { a } = { x } )
48 47 oveq1d 
 |-  ( a = x -> ( { a } .(+) N ) = ( { x } .(+) N ) )
49 48 eleq1d 
 |-  ( a = x -> ( ( { a } .(+) N ) e. F <-> ( { x } .(+) N ) e. F ) )
50 49 elrab 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. F } <-> ( x e. B /\ ( { x } .(+) N ) e. F ) )
51 50 simprbi 
 |-  ( x e. { a e. B | ( { a } .(+) N ) e. F } -> ( { x } .(+) N ) e. F )
52 51 ad2antlr 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( { x } .(+) N ) e. F )
53 46 52 eqeltrd 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> [ x ] ( G ~QG N ) e. F )
54 1 3 39 35 quslsm 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> [ y ] ( G ~QG N ) = ( { y } .(+) N ) )
55 sneq 
 |-  ( a = y -> { a } = { y } )
56 55 oveq1d 
 |-  ( a = y -> ( { a } .(+) N ) = ( { y } .(+) N ) )
57 56 eleq1d 
 |-  ( a = y -> ( ( { a } .(+) N ) e. F <-> ( { y } .(+) N ) e. F ) )
58 57 elrab 
 |-  ( y e. { a e. B | ( { a } .(+) N ) e. F } <-> ( y e. B /\ ( { y } .(+) N ) e. F ) )
59 58 simprbi 
 |-  ( y e. { a e. B | ( { a } .(+) N ) e. F } -> ( { y } .(+) N ) e. F )
60 59 adantl 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( { y } .(+) N ) e. F )
61 54 60 eqeltrd 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> [ y ] ( G ~QG N ) e. F )
62 42 subgcl 
 |-  ( ( F e. ( SubGrp ` Q ) /\ [ x ] ( G ~QG N ) e. F /\ [ y ] ( G ~QG N ) e. F ) -> ( [ x ] ( G ~QG N ) ( +g ` Q ) [ y ] ( G ~QG N ) ) e. F )
63 45 53 61 62 syl3anc 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( [ x ] ( G ~QG N ) ( +g ` Q ) [ y ] ( G ~QG N ) ) e. F )
64 44 63 eqeltrrd 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> [ ( x ( +g ` G ) y ) ] ( G ~QG N ) e. F )
65 40 64 eqeltrrd 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( { ( x ( +g ` G ) y ) } .(+) N ) e. F )
66 30 38 65 elrabd 
 |-  ( ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( x ( +g ` G ) y ) e. { a e. B | ( { a } .(+) N ) e. F } )
67 66 3impa 
 |-  ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } /\ y e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( x ( +g ` G ) y ) e. { a e. B | ( { a } .(+) N ) e. F } )
68 sneq 
 |-  ( a = ( ( invg ` G ) ` x ) -> { a } = { ( ( invg ` G ) ` x ) } )
69 68 oveq1d 
 |-  ( a = ( ( invg ` G ) ` x ) -> ( { a } .(+) N ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
70 69 eleq1d 
 |-  ( a = ( ( invg ` G ) ` x ) -> ( ( { a } .(+) N ) e. F <-> ( { ( ( invg ` G ) ` x ) } .(+) N ) e. F ) )
71 eqid 
 |-  ( invg ` G ) = ( invg ` G )
72 1 71 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
73 18 72 sylan 
 |-  ( ( ph /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
74 73 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> ( ( invg ` G ) ` x ) e. B )
75 eqid 
 |-  ( invg ` Q ) = ( invg ` Q )
76 2 1 71 75 qusinv 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ x e. B ) -> ( ( invg ` Q ) ` [ x ] ( G ~QG N ) ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) )
77 4 76 sylan 
 |-  ( ( ph /\ x e. B ) -> ( ( invg ` Q ) ` [ x ] ( G ~QG N ) ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) )
78 16 adantr 
 |-  ( ( ph /\ x e. B ) -> N e. ( SubGrp ` G ) )
79 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
80 1 3 78 79 quslsm 
 |-  ( ( ph /\ x e. B ) -> [ x ] ( G ~QG N ) = ( { x } .(+) N ) )
81 80 fveq2d 
 |-  ( ( ph /\ x e. B ) -> ( ( invg ` Q ) ` [ x ] ( G ~QG N ) ) = ( ( invg ` Q ) ` ( { x } .(+) N ) ) )
82 1 3 78 73 quslsm 
 |-  ( ( ph /\ x e. B ) -> [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
83 77 81 82 3eqtr3d 
 |-  ( ( ph /\ x e. B ) -> ( ( invg ` Q ) ` ( { x } .(+) N ) ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
84 83 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> ( ( invg ` Q ) ` ( { x } .(+) N ) ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
85 5 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> F e. ( SubGrp ` Q ) )
86 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> ( { x } .(+) N ) e. F )
87 75 subginvcl 
 |-  ( ( F e. ( SubGrp ` Q ) /\ ( { x } .(+) N ) e. F ) -> ( ( invg ` Q ) ` ( { x } .(+) N ) ) e. F )
88 85 86 87 syl2anc 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> ( ( invg ` Q ) ` ( { x } .(+) N ) ) e. F )
89 84 88 eqeltrrd 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> ( { ( ( invg ` G ) ` x ) } .(+) N ) e. F )
90 70 74 89 elrabd 
 |-  ( ( ( ph /\ x e. B ) /\ ( { x } .(+) N ) e. F ) -> ( ( invg ` G ) ` x ) e. { a e. B | ( { a } .(+) N ) e. F } )
91 90 anasss 
 |-  ( ( ph /\ ( x e. B /\ ( { x } .(+) N ) e. F ) ) -> ( ( invg ` G ) ` x ) e. { a e. B | ( { a } .(+) N ) e. F } )
92 50 91 sylan2b 
 |-  ( ( ph /\ x e. { a e. B | ( { a } .(+) N ) e. F } ) -> ( ( invg ` G ) ` x ) e. { a e. B | ( { a } .(+) N ) e. F } )
93 6 7 8 11 27 67 92 18 issubgrpd2 
 |-  ( ph -> { a e. B | ( { a } .(+) N ) e. F } e. ( SubGrp ` G ) )