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

Metamath Proof Explorer

Theorem nsgqusf1olem1

Description: Lemma for nsgqusf1o . (Contributed by Thierry Arnoux, 4-Aug-2024)

Ref Expression
Hypotheses nsgqusf1o.b 
|- B = ( Base ` G )
nsgqusf1o.s 
|- S = { h e. ( SubGrp ` G ) | N C_ h }
nsgqusf1o.t 
|- T = ( SubGrp ` Q )
nsgqusf1o.1 
|- .<_ = ( le ` ( toInc ` S ) )
nsgqusf1o.2 
|- .c_ = ( le ` ( toInc ` T ) )
nsgqusf1o.q 
|- Q = ( G /s ( G ~QG N ) )
nsgqusf1o.p 
|- .(+) = ( LSSum ` G )
nsgqusf1o.e 
|- E = ( h e. S |-> ran ( x e. h |-> ( { x } .(+) N ) ) )
nsgqusf1o.f 
|- F = ( f e. T |-> { a e. B | ( { a } .(+) N ) e. f } )
nsgqusf1o.n 
|- ( ph -> N e. ( NrmSGrp ` G ) )
Assertion nsgqusf1olem1 
|- ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. T )

Proof

Step Hyp Ref Expression
1 nsgqusf1o.b 
 |-  B = ( Base ` G )
2 nsgqusf1o.s 
 |-  S = { h e. ( SubGrp ` G ) | N C_ h }
3 nsgqusf1o.t 
 |-  T = ( SubGrp ` Q )
4 nsgqusf1o.1 
 |-  .<_ = ( le ` ( toInc ` S ) )
5 nsgqusf1o.2 
 |-  .c_ = ( le ` ( toInc ` T ) )
6 nsgqusf1o.q 
 |-  Q = ( G /s ( G ~QG N ) )
7 nsgqusf1o.p 
 |-  .(+) = ( LSSum ` G )
8 nsgqusf1o.e 
 |-  E = ( h e. S |-> ran ( x e. h |-> ( { x } .(+) N ) ) )
9 nsgqusf1o.f 
 |-  F = ( f e. T |-> { a e. B | ( { a } .(+) N ) e. f } )
10 nsgqusf1o.n 
 |-  ( ph -> N e. ( NrmSGrp ` G ) )
11 6 qusgrp 
 |-  ( N e. ( NrmSGrp ` G ) -> Q e. Grp )
12 10 11 syl 
 |-  ( ph -> Q e. Grp )
13 12 ad2antrr 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> Q e. Grp )
14 1 subgss 
 |-  ( h e. ( SubGrp ` G ) -> h C_ B )
15 14 ad2antlr 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> h C_ B )
16 15 sselda 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> x e. B )
17 ovex 
 |-  ( G ~QG N ) e. _V
18 17 ecelqsi 
 |-  ( x e. B -> [ x ] ( G ~QG N ) e. ( B /. ( G ~QG N ) ) )
19 16 18 syl 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> [ x ] ( G ~QG N ) e. ( B /. ( G ~QG N ) ) )
20 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
21 10 20 syl 
 |-  ( ph -> N e. ( SubGrp ` G ) )
22 21 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> N e. ( SubGrp ` G ) )
23 1 7 22 16 quslsm 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> [ x ] ( G ~QG N ) = ( { x } .(+) N ) )
24 6 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG N ) ) )
25 1 a1i 
 |-  ( ph -> B = ( Base ` G ) )
26 ovexd 
 |-  ( ph -> ( G ~QG N ) e. _V )
27 subgrcl 
 |-  ( N e. ( SubGrp ` G ) -> G e. Grp )
28 21 27 syl 
 |-  ( ph -> G e. Grp )
29 24 25 26 28 qusbas 
 |-  ( ph -> ( B /. ( G ~QG N ) ) = ( Base ` Q ) )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> ( B /. ( G ~QG N ) ) = ( Base ` Q ) )
31 19 23 30 3eltr3d 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> ( { x } .(+) N ) e. ( Base ` Q ) )
32 31 ralrimiva 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> A. x e. h ( { x } .(+) N ) e. ( Base ` Q ) )
33 eqid 
 |-  ( x e. h |-> ( { x } .(+) N ) ) = ( x e. h |-> ( { x } .(+) N ) )
34 33 rnmptss 
 |-  ( A. x e. h ( { x } .(+) N ) e. ( Base ` Q ) -> ran ( x e. h |-> ( { x } .(+) N ) ) C_ ( Base ` Q ) )
35 32 34 syl 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> ran ( x e. h |-> ( { x } .(+) N ) ) C_ ( Base ` Q ) )
36 nfv 
 |-  F/ x ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h )
37 ovexd 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> ( { x } .(+) N ) e. _V )
38 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
39 38 subg0cl 
 |-  ( h e. ( SubGrp ` G ) -> ( 0g ` G ) e. h )
40 39 ne0d 
 |-  ( h e. ( SubGrp ` G ) -> h =/= (/) )
41 40 ad2antlr 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> h =/= (/) )
42 36 37 33 41 rnmptn0 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> ran ( x e. h |-> ( { x } .(+) N ) ) =/= (/) )
43 nfmpt1 
 |-  F/_ x ( x e. h |-> ( { x } .(+) N ) )
44 43 nfrn 
 |-  F/_ x ran ( x e. h |-> ( { x } .(+) N ) )
45 44 nfel2 
 |-  F/ x i e. ran ( x e. h |-> ( { x } .(+) N ) )
46 36 45 nfan 
 |-  F/ x ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ i e. ran ( x e. h |-> ( { x } .(+) N ) ) )
47 44 nfel2 
 |-  F/ x ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) )
48 44 47 nfralw 
 |-  F/ x A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) )
49 44 nfel2 
 |-  F/ x ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) )
50 48 49 nfan 
 |-  F/ x ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
51 sneq 
 |-  ( x = z -> { x } = { z } )
52 51 oveq1d 
 |-  ( x = z -> ( { x } .(+) N ) = ( { z } .(+) N ) )
53 52 cbvmptv 
 |-  ( x e. h |-> ( { x } .(+) N ) ) = ( z e. h |-> ( { z } .(+) N ) )
54 simp-4r 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> h e. ( SubGrp ` G ) )
55 54 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> h e. ( SubGrp ` G ) )
56 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> x e. h )
57 simplr 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> y e. h )
58 eqid 
 |-  ( +g ` G ) = ( +g ` G )
59 58 subgcl 
 |-  ( ( h e. ( SubGrp ` G ) /\ x e. h /\ y e. h ) -> ( x ( +g ` G ) y ) e. h )
60 55 56 57 59 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( x ( +g ` G ) y ) e. h )
61 sneq 
 |-  ( z = ( x ( +g ` G ) y ) -> { z } = { ( x ( +g ` G ) y ) } )
62 61 oveq1d 
 |-  ( z = ( x ( +g ` G ) y ) -> ( { z } .(+) N ) = ( { ( x ( +g ` G ) y ) } .(+) N ) )
63 62 eqeq2d 
 |-  ( z = ( x ( +g ` G ) y ) -> ( ( i ( +g ` Q ) j ) = ( { z } .(+) N ) <-> ( i ( +g ` Q ) j ) = ( { ( x ( +g ` G ) y ) } .(+) N ) ) )
64 63 adantl 
 |-  ( ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) /\ z = ( x ( +g ` G ) y ) ) -> ( ( i ( +g ` Q ) j ) = ( { z } .(+) N ) <-> ( i ( +g ` Q ) j ) = ( { ( x ( +g ` G ) y ) } .(+) N ) ) )
65 simpr 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> i = ( { x } .(+) N ) )
66 23 adantr 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> [ x ] ( G ~QG N ) = ( { x } .(+) N ) )
67 65 66 eqtr4d 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> i = [ x ] ( G ~QG N ) )
68 67 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> i = [ x ] ( G ~QG N ) )
69 simpr 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> j = ( { y } .(+) N ) )
70 10 ad4antr 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> N e. ( NrmSGrp ` G ) )
71 70 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> N e. ( NrmSGrp ` G ) )
72 71 20 syl 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> N e. ( SubGrp ` G ) )
73 55 14 syl 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> h C_ B )
74 73 57 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> y e. B )
75 1 7 72 74 quslsm 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> [ y ] ( G ~QG N ) = ( { y } .(+) N ) )
76 69 75 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> j = [ y ] ( G ~QG N ) )
77 68 76 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( i ( +g ` Q ) j ) = ( [ x ] ( G ~QG N ) ( +g ` Q ) [ y ] ( G ~QG N ) ) )
78 16 adantr 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> x e. B )
79 78 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> x e. B )
80 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
81 6 1 58 80 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 ) )
82 71 79 74 81 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( [ x ] ( G ~QG N ) ( +g ` Q ) [ y ] ( G ~QG N ) ) = [ ( x ( +g ` G ) y ) ] ( G ~QG N ) )
83 73 60 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( x ( +g ` G ) y ) e. B )
84 1 7 72 83 quslsm 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> [ ( x ( +g ` G ) y ) ] ( G ~QG N ) = ( { ( x ( +g ` G ) y ) } .(+) N ) )
85 77 82 84 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( i ( +g ` Q ) j ) = ( { ( x ( +g ` G ) y ) } .(+) N ) )
86 60 64 85 rspcedvd 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> E. z e. h ( i ( +g ` Q ) j ) = ( { z } .(+) N ) )
87 ovexd 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( i ( +g ` Q ) j ) e. _V )
88 53 86 87 elrnmptd 
 |-  ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
89 88 adantllr 
 |-  ( ( ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ j e. ran ( x e. h |-> ( { x } .(+) N ) ) ) /\ y e. h ) /\ j = ( { y } .(+) N ) ) -> ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
90 sneq 
 |-  ( x = y -> { x } = { y } )
91 90 oveq1d 
 |-  ( x = y -> ( { x } .(+) N ) = ( { y } .(+) N ) )
92 91 cbvmptv 
 |-  ( x e. h |-> ( { x } .(+) N ) ) = ( y e. h |-> ( { y } .(+) N ) )
93 ovex 
 |-  ( { y } .(+) N ) e. _V
94 92 93 elrnmpti 
 |-  ( j e. ran ( x e. h |-> ( { x } .(+) N ) ) <-> E. y e. h j = ( { y } .(+) N ) )
95 94 biimpi 
 |-  ( j e. ran ( x e. h |-> ( { x } .(+) N ) ) -> E. y e. h j = ( { y } .(+) N ) )
96 95 adantl 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ j e. ran ( x e. h |-> ( { x } .(+) N ) ) ) -> E. y e. h j = ( { y } .(+) N ) )
97 89 96 r19.29a 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ j e. ran ( x e. h |-> ( { x } .(+) N ) ) ) -> ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
98 97 ralrimiva 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
99 eqid 
 |-  ( invg ` G ) = ( invg ` G )
100 99 subginvcl 
 |-  ( ( h e. ( SubGrp ` G ) /\ x e. h ) -> ( ( invg ` G ) ` x ) e. h )
101 100 ad5ant24 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( ( invg ` G ) ` x ) e. h )
102 simpr 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y = ( ( invg ` G ) ` x ) ) -> y = ( ( invg ` G ) ` x ) )
103 102 sneqd 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y = ( ( invg ` G ) ` x ) ) -> { y } = { ( ( invg ` G ) ` x ) } )
104 103 oveq1d 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y = ( ( invg ` G ) ` x ) ) -> ( { y } .(+) N ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
105 15 adantr 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> h C_ B )
106 100 ad4ant24 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> ( ( invg ` G ) ` x ) e. h )
107 105 106 sseldd 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> ( ( invg ` G ) ` x ) e. B )
108 1 7 22 107 quslsm 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) -> [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
109 108 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y = ( ( invg ` G ) ` x ) ) -> [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) = ( { ( ( invg ` G ) ` x ) } .(+) N ) )
110 104 109 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y = ( ( invg ` G ) ` x ) ) -> ( { y } .(+) N ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) )
111 110 eqeq2d 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) /\ y = ( ( invg ` G ) ` x ) ) -> ( ( ( invg ` Q ) ` i ) = ( { y } .(+) N ) <-> ( ( invg ` Q ) ` i ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) ) )
112 67 fveq2d 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( ( invg ` Q ) ` i ) = ( ( invg ` Q ) ` [ x ] ( G ~QG N ) ) )
113 eqid 
 |-  ( invg ` Q ) = ( invg ` Q )
114 6 1 99 113 qusinv 
 |-  ( ( N e. ( NrmSGrp ` G ) /\ x e. B ) -> ( ( invg ` Q ) ` [ x ] ( G ~QG N ) ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) )
115 70 78 114 syl2anc 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( ( invg ` Q ) ` [ x ] ( G ~QG N ) ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) )
116 112 115 eqtrd 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( ( invg ` Q ) ` i ) = [ ( ( invg ` G ) ` x ) ] ( G ~QG N ) )
117 101 111 116 rspcedvd 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> E. y e. h ( ( invg ` Q ) ` i ) = ( { y } .(+) N ) )
118 fvexd 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( ( invg ` Q ) ` i ) e. _V )
119 92 117 118 elrnmptd 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) )
120 98 119 jca 
 |-  ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) ) )
121 120 adantllr 
 |-  ( ( ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ i e. ran ( x e. h |-> ( { x } .(+) N ) ) ) /\ x e. h ) /\ i = ( { x } .(+) N ) ) -> ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) ) )
122 ovex 
 |-  ( { x } .(+) N ) e. _V
123 33 122 elrnmpti 
 |-  ( i e. ran ( x e. h |-> ( { x } .(+) N ) ) <-> E. x e. h i = ( { x } .(+) N ) )
124 123 biimpi 
 |-  ( i e. ran ( x e. h |-> ( { x } .(+) N ) ) -> E. x e. h i = ( { x } .(+) N ) )
125 124 adantl 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ i e. ran ( x e. h |-> ( { x } .(+) N ) ) ) -> E. x e. h i = ( { x } .(+) N ) )
126 46 50 121 125 r19.29af2 
 |-  ( ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) /\ i e. ran ( x e. h |-> ( { x } .(+) N ) ) ) -> ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) ) )
127 126 ralrimiva 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> A. i e. ran ( x e. h |-> ( { x } .(+) N ) ) ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) ) )
128 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
129 128 80 113 issubg2 
 |-  ( Q e. Grp -> ( ran ( x e. h |-> ( { x } .(+) N ) ) e. ( SubGrp ` Q ) <-> ( ran ( x e. h |-> ( { x } .(+) N ) ) C_ ( Base ` Q ) /\ ran ( x e. h |-> ( { x } .(+) N ) ) =/= (/) /\ A. i e. ran ( x e. h |-> ( { x } .(+) N ) ) ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) ) ) ) )
130 129 biimpar 
 |-  ( ( Q e. Grp /\ ( ran ( x e. h |-> ( { x } .(+) N ) ) C_ ( Base ` Q ) /\ ran ( x e. h |-> ( { x } .(+) N ) ) =/= (/) /\ A. i e. ran ( x e. h |-> ( { x } .(+) N ) ) ( A. j e. ran ( x e. h |-> ( { x } .(+) N ) ) ( i ( +g ` Q ) j ) e. ran ( x e. h |-> ( { x } .(+) N ) ) /\ ( ( invg ` Q ) ` i ) e. ran ( x e. h |-> ( { x } .(+) N ) ) ) ) ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. ( SubGrp ` Q ) )
131 13 35 42 127 130 syl13anc 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. ( SubGrp ` Q ) )
132 131 3 eleqtrrdi 
 |-  ( ( ( ph /\ h e. ( SubGrp ` G ) ) /\ N C_ h ) -> ran ( x e. h |-> ( { x } .(+) N ) ) e. T )