Metamath Proof Explorer

Theorem qustgplem

Description: Lemma for qustgp . (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qustgp.h 
|- H = ( G /s ( G ~QG Y ) )
qustgpopn.x 
|- X = ( Base ` G )
qustgpopn.j 
|- J = ( TopOpen ` G )
qustgpopn.k 
|- K = ( TopOpen ` H )
qustgpopn.f 
|- F = ( x e. X |-> [ x ] ( G ~QG Y ) )
qustgplem.m 
|- .- = ( z e. X , w e. X |-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
Assertion qustgplem 
|- ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp )

Proof

Step Hyp Ref Expression
1 qustgp.h 
 |-  H = ( G /s ( G ~QG Y ) )
2 qustgpopn.x 
 |-  X = ( Base ` G )
3 qustgpopn.j 
 |-  J = ( TopOpen ` G )
4 qustgpopn.k 
 |-  K = ( TopOpen ` H )
5 qustgpopn.f 
 |-  F = ( x e. X |-> [ x ] ( G ~QG Y ) )
6 qustgplem.m 
 |-  .- = ( z e. X , w e. X |-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
7 1 qusgrp 
 |-  ( Y e. ( NrmSGrp ` G ) -> H e. Grp )
8 7 adantl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. Grp )
9 1 a1i 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H = ( G /s ( G ~QG Y ) ) )
10 2 a1i 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> X = ( Base ` G ) )
11 ovex 
 |-  ( G ~QG Y ) e. _V
12 11 a1i 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( G ~QG Y ) e. _V )
13 simpl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> G e. TopGrp )
14 9 10 5 12 13 qusval 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H = ( F "s G ) )
15 9 10 5 12 13 quslem 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> F : X -onto-> ( X /. ( G ~QG Y ) ) )
16 14 10 15 13 3 4 imastopn 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> K = ( J qTop F ) )
17 3 2 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
18 17 adantr 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> J e. ( TopOn ` X ) )
19 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> ( X /. ( G ~QG Y ) ) ) -> ( J qTop F ) e. ( TopOn ` ( X /. ( G ~QG Y ) ) ) )
20 18 15 19 syl2anc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( J qTop F ) e. ( TopOn ` ( X /. ( G ~QG Y ) ) ) )
21 16 20 eqeltrd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> K e. ( TopOn ` ( X /. ( G ~QG Y ) ) ) )
22 9 10 12 13 qusbas 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( X /. ( G ~QG Y ) ) = ( Base ` H ) )
23 22 fveq2d 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( TopOn ` ( X /. ( G ~QG Y ) ) ) = ( TopOn ` ( Base ` H ) ) )
24 21 23 eleqtrd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> K e. ( TopOn ` ( Base ` H ) ) )
25 eqid 
 |-  ( Base ` H ) = ( Base ` H )
26 25 4 istps 
 |-  ( H e. TopSp <-> K e. ( TopOn ` ( Base ` H ) ) )
27 24 26 sylibr 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopSp )
28 eqid 
 |-  ( -g ` H ) = ( -g ` H )
29 25 28 grpsubf 
 |-  ( H e. Grp -> ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
30 8 29 syl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
31 cnvimass 
 |-  ( `' ( -g ` H ) " u ) C_ dom ( -g ` H )
32 30 fdmd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> dom ( -g ` H ) = ( ( Base ` H ) X. ( Base ` H ) ) )
33 32 adantr 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> dom ( -g ` H ) = ( ( Base ` H ) X. ( Base ` H ) ) )
34 31 33 sseqtrid 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( `' ( -g ` H ) " u ) C_ ( ( Base ` H ) X. ( Base ` H ) ) )
35 relxp 
 |-  Rel ( ( Base ` H ) X. ( Base ` H ) )
36 relss 
 |-  ( ( `' ( -g ` H ) " u ) C_ ( ( Base ` H ) X. ( Base ` H ) ) -> ( Rel ( ( Base ` H ) X. ( Base ` H ) ) -> Rel ( `' ( -g ` H ) " u ) ) )
37 34 35 36 mpisyl 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> Rel ( `' ( -g ` H ) " u ) )
38 34 sseld 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) ) )
39 vex 
 |-  x e. _V
40 39 elqs 
 |-  ( x e. ( X /. ( G ~QG Y ) ) <-> E. a e. X x = [ a ] ( G ~QG Y ) )
41 22 adantr 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( X /. ( G ~QG Y ) ) = ( Base ` H ) )
42 41 eleq2d 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( x e. ( X /. ( G ~QG Y ) ) <-> x e. ( Base ` H ) ) )
43 40 42 bitr3id 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. a e. X x = [ a ] ( G ~QG Y ) <-> x e. ( Base ` H ) ) )
44 vex 
 |-  y e. _V
45 44 elqs 
 |-  ( y e. ( X /. ( G ~QG Y ) ) <-> E. b e. X y = [ b ] ( G ~QG Y ) )
46 41 eleq2d 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( y e. ( X /. ( G ~QG Y ) ) <-> y e. ( Base ` H ) ) )
47 45 46 bitr3id 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. b e. X y = [ b ] ( G ~QG Y ) <-> y e. ( Base ` H ) ) )
48 43 47 anbi12d 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( ( E. a e. X x = [ a ] ( G ~QG Y ) /\ E. b e. X y = [ b ] ( G ~QG Y ) ) <-> ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) ) )
49 reeanv 
 |-  ( E. a e. X E. b e. X ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) <-> ( E. a e. X x = [ a ] ( G ~QG Y ) /\ E. b e. X y = [ b ] ( G ~QG Y ) ) )
50 opelxp 
 |-  ( <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) <-> ( x e. ( Base ` H ) /\ y e. ( Base ` H ) ) )
51 48 49 50 3bitr4g 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. a e. X E. b e. X ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) <-> <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) ) )
52 8 ad2antrr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> H e. Grp )
53 52 29 syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
54 ffn 
 |-  ( ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) -> ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) )
55 elpreima 
 |-  ( ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u ) ) )
56 53 54 55 3syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u ) ) )
57 df-ov 
 |-  ( [ a ] ( G ~QG Y ) ( -g ` H ) [ b ] ( G ~QG Y ) ) = ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. )
58 simpllr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> Y e. ( NrmSGrp ` G ) )
59 simprl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> a e. X )
60 simprr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> b e. X )
61 eqid 
 |-  ( -g ` G ) = ( -g ` G )
62 1 2 61 28 qussub 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ a e. X /\ b e. X ) -> ( [ a ] ( G ~QG Y ) ( -g ` H ) [ b ] ( G ~QG Y ) ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
63 58 59 60 62 syl3anc 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( [ a ] ( G ~QG Y ) ( -g ` H ) [ b ] ( G ~QG Y ) ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
64 57 63 eqtr3id 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
65 64 eleq1d 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u <-> [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
66 simpr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( a e. X /\ b e. X ) )
67 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
68 67 adantr 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> G e. Grp )
69 2 61 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( X X. X ) --> X )
70 ffn 
 |-  ( ( -g ` G ) : ( X X. X ) --> X -> ( -g ` G ) Fn ( X X. X ) )
71 68 69 70 3syl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` G ) Fn ( X X. X ) )
72 fnov 
 |-  ( ( -g ` G ) Fn ( X X. X ) <-> ( -g ` G ) = ( z e. X , w e. X |-> ( z ( -g ` G ) w ) ) )
73 71 72 sylib 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` G ) = ( z e. X , w e. X |-> ( z ( -g ` G ) w ) ) )
74 3 61 tgpsubcn 
 |-  ( G e. TopGrp -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
75 74 adantr 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
76 73 75 eqeltrrd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( z e. X , w e. X |-> ( z ( -g ` G ) w ) ) e. ( ( J tX J ) Cn J ) )
77 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ x ] ( G ~QG Y ) e. _V )
78 11 77 ax-mp 
 |-  [ x ] ( G ~QG Y ) e. _V
79 78 5 fnmpti 
 |-  F Fn X
80 qtopid 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
81 18 79 80 sylancl 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> F e. ( J Cn ( J qTop F ) ) )
82 16 oveq2d 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( J Cn K ) = ( J Cn ( J qTop F ) ) )
83 81 82 eleqtrrd 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> F e. ( J Cn K ) )
84 5 83 eqeltrrid 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( x e. X |-> [ x ] ( G ~QG Y ) ) e. ( J Cn K ) )
85 eceq1 
 |-  ( x = ( z ( -g ` G ) w ) -> [ x ] ( G ~QG Y ) = [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) )
86 18 18 76 18 84 85 cnmpt21 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( z e. X , w e. X |-> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) ) e. ( ( J tX J ) Cn K ) )
87 6 86 eqeltrid 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> .- e. ( ( J tX J ) Cn K ) )
88 87 ad2antrr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> .- e. ( ( J tX J ) Cn K ) )
89 simplr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> u e. K )
90 cnima 
 |-  ( ( .- e. ( ( J tX J ) Cn K ) /\ u e. K ) -> ( `' .- " u ) e. ( J tX J ) )
91 88 89 90 syl2anc 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( `' .- " u ) e. ( J tX J ) )
92 18 ad2antrr 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> J e. ( TopOn ` X ) )
93 eltx 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. ( TopOn ` X ) ) -> ( ( `' .- " u ) e. ( J tX J ) <-> A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
94 92 92 93 syl2anc 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( `' .- " u ) e. ( J tX J ) <-> A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
95 91 94 mpbid 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) )
96 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) e. _V )
97 11 96 ax-mp 
 |-  [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) e. _V
98 6 97 fnmpoi 
 |-  .- Fn ( X X. X )
99 elpreima 
 |-  ( .- Fn ( X X. X ) -> ( <. a , b >. e. ( `' .- " u ) <-> ( <. a , b >. e. ( X X. X ) /\ ( .- ` <. a , b >. ) e. u ) ) )
100 98 99 ax-mp 
 |-  ( <. a , b >. e. ( `' .- " u ) <-> ( <. a , b >. e. ( X X. X ) /\ ( .- ` <. a , b >. ) e. u ) )
101 opelxp 
 |-  ( <. a , b >. e. ( X X. X ) <-> ( a e. X /\ b e. X ) )
102 101 anbi1i 
 |-  ( ( <. a , b >. e. ( X X. X ) /\ ( .- ` <. a , b >. ) e. u ) <-> ( ( a e. X /\ b e. X ) /\ ( .- ` <. a , b >. ) e. u ) )
103 df-ov 
 |-  ( a .- b ) = ( .- ` <. a , b >. )
104 oveq12 
 |-  ( ( z = a /\ w = b ) -> ( z ( -g ` G ) w ) = ( a ( -g ` G ) b ) )
105 104 eceq1d 
 |-  ( ( z = a /\ w = b ) -> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
106 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. _V )
107 11 106 ax-mp 
 |-  [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. _V
108 105 6 107 ovmpoa 
 |-  ( ( a e. X /\ b e. X ) -> ( a .- b ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
109 103 108 eqtr3id 
 |-  ( ( a e. X /\ b e. X ) -> ( .- ` <. a , b >. ) = [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) )
110 109 eleq1d 
 |-  ( ( a e. X /\ b e. X ) -> ( ( .- ` <. a , b >. ) e. u <-> [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
111 110 pm5.32i 
 |-  ( ( ( a e. X /\ b e. X ) /\ ( .- ` <. a , b >. ) e. u ) <-> ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
112 100 102 111 3bitri 
 |-  ( <. a , b >. e. ( `' .- " u ) <-> ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) )
113 eleq1 
 |-  ( t = <. a , b >. -> ( t e. ( c X. d ) <-> <. a , b >. e. ( c X. d ) ) )
114 opelxp 
 |-  ( <. a , b >. e. ( c X. d ) <-> ( a e. c /\ b e. d ) )
115 113 114 bitrdi 
 |-  ( t = <. a , b >. -> ( t e. ( c X. d ) <-> ( a e. c /\ b e. d ) ) )
116 115 anbi1d 
 |-  ( t = <. a , b >. -> ( ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) <-> ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
117 116 2rexbidv 
 |-  ( t = <. a , b >. -> ( E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) <-> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
118 117 rspccv 
 |-  ( A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> ( <. a , b >. e. ( `' .- " u ) -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
119 112 118 syl5bir 
 |-  ( A. t e. ( `' .- " u ) E. c e. J E. d e. J ( t e. ( c X. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> ( ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
120 95 119 syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( a e. X /\ b e. X ) /\ [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u ) -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
121 66 120 mpand 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u -> E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) )
122 simp-4l 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> G e. TopGrp )
123 58 adantr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> Y e. ( NrmSGrp ` G ) )
124 simprll 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> c e. J )
125 1 2 3 4 5 qustgpopn 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ c e. J ) -> ( F " c ) e. K )
126 122 123 124 125 syl3anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F " c ) e. K )
127 simprlr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> d e. J )
128 1 2 3 4 5 qustgpopn 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) /\ d e. J ) -> ( F " d ) e. K )
129 122 123 127 128 syl3anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F " d ) e. K )
130 59 adantr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> a e. X )
131 eceq1 
 |-  ( x = a -> [ x ] ( G ~QG Y ) = [ a ] ( G ~QG Y ) )
132 131 5 78 fvmpt3i 
 |-  ( a e. X -> ( F ` a ) = [ a ] ( G ~QG Y ) )
133 130 132 syl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` a ) = [ a ] ( G ~QG Y ) )
134 122 17 syl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> J e. ( TopOn ` X ) )
135 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ c e. J ) -> c C_ X )
136 134 124 135 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> c C_ X )
137 simprrl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( a e. c /\ b e. d ) )
138 137 simpld 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> a e. c )
139 fnfvima 
 |-  ( ( F Fn X /\ c C_ X /\ a e. c ) -> ( F ` a ) e. ( F " c ) )
140 79 136 138 139 mp3an2i 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` a ) e. ( F " c ) )
141 133 140 eqeltrrd 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> [ a ] ( G ~QG Y ) e. ( F " c ) )
142 60 adantr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> b e. X )
143 eceq1 
 |-  ( x = b -> [ x ] ( G ~QG Y ) = [ b ] ( G ~QG Y ) )
144 143 5 78 fvmpt3i 
 |-  ( b e. X -> ( F ` b ) = [ b ] ( G ~QG Y ) )
145 142 144 syl 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` b ) = [ b ] ( G ~QG Y ) )
146 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ d e. J ) -> d C_ X )
147 134 127 146 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> d C_ X )
148 137 simprd 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> b e. d )
149 fnfvima 
 |-  ( ( F Fn X /\ d C_ X /\ b e. d ) -> ( F ` b ) e. ( F " d ) )
150 79 147 148 149 mp3an2i 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( F ` b ) e. ( F " d ) )
151 145 150 eqeltrrd 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> [ b ] ( G ~QG Y ) e. ( F " d ) )
152 141 151 opelxpd 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) )
153 136 sselda 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ p e. c ) -> p e. X )
154 147 sselda 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ q e. d ) -> q e. X )
155 153 154 anim12dan 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( p e. X /\ q e. X ) )
156 eceq1 
 |-  ( x = p -> [ x ] ( G ~QG Y ) = [ p ] ( G ~QG Y ) )
157 156 5 78 fvmpt3i 
 |-  ( p e. X -> ( F ` p ) = [ p ] ( G ~QG Y ) )
158 eceq1 
 |-  ( x = q -> [ x ] ( G ~QG Y ) = [ q ] ( G ~QG Y ) )
159 158 5 78 fvmpt3i 
 |-  ( q e. X -> ( F ` q ) = [ q ] ( G ~QG Y ) )
160 opeq12 
 |-  ( ( ( F ` p ) = [ p ] ( G ~QG Y ) /\ ( F ` q ) = [ q ] ( G ~QG Y ) ) -> <. ( F ` p ) , ( F ` q ) >. = <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
161 157 159 160 syl2an 
 |-  ( ( p e. X /\ q e. X ) -> <. ( F ` p ) , ( F ` q ) >. = <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
162 155 161 syl 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. ( F ` p ) , ( F ` q ) >. = <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
163 123 adantr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> Y e. ( NrmSGrp ` G ) )
164 1 2 25 quseccl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ p e. X ) -> [ p ] ( G ~QG Y ) e. ( Base ` H ) )
165 1 2 25 quseccl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ q e. X ) -> [ q ] ( G ~QG Y ) e. ( Base ` H ) )
166 164 165 anim12dan 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( p e. X /\ q e. X ) ) -> ( [ p ] ( G ~QG Y ) e. ( Base ` H ) /\ [ q ] ( G ~QG Y ) e. ( Base ` H ) ) )
167 163 155 166 syl2anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( [ p ] ( G ~QG Y ) e. ( Base ` H ) /\ [ q ] ( G ~QG Y ) e. ( Base ` H ) ) )
168 opelxpi 
 |-  ( ( [ p ] ( G ~QG Y ) e. ( Base ` H ) /\ [ q ] ( G ~QG Y ) e. ( Base ` H ) ) -> <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) )
169 167 168 syl 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) )
170 1 2 61 28 qussub 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ p e. X /\ q e. X ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
171 170 3expb 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( p e. X /\ q e. X ) ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
172 163 155 171 syl2anc 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
173 oveq12 
 |-  ( ( z = p /\ w = q ) -> ( z ( -g ` G ) w ) = ( p ( -g ` G ) q ) )
174 173 eceq1d 
 |-  ( ( z = p /\ w = q ) -> [ ( z ( -g ` G ) w ) ] ( G ~QG Y ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
175 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) e. _V )
176 11 175 ax-mp 
 |-  [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) e. _V
177 174 6 176 ovmpoa 
 |-  ( ( p e. X /\ q e. X ) -> ( p .- q ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
178 155 177 syl 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( p .- q ) = [ ( p ( -g ` G ) q ) ] ( G ~QG Y ) )
179 172 178 eqtr4d 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = ( p .- q ) )
180 df-ov 
 |-  ( [ p ] ( G ~QG Y ) ( -g ` H ) [ q ] ( G ~QG Y ) ) = ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. )
181 df-ov 
 |-  ( p .- q ) = ( .- ` <. p , q >. )
182 179 180 181 3eqtr3g 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) = ( .- ` <. p , q >. ) )
183 opelxpi 
 |-  ( ( p e. c /\ q e. d ) -> <. p , q >. e. ( c X. d ) )
184 simprrr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( c X. d ) C_ ( `' .- " u ) )
185 184 sselda 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ <. p , q >. e. ( c X. d ) ) -> <. p , q >. e. ( `' .- " u ) )
186 183 185 sylan2 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. p , q >. e. ( `' .- " u ) )
187 elpreima 
 |-  ( .- Fn ( X X. X ) -> ( <. p , q >. e. ( `' .- " u ) <-> ( <. p , q >. e. ( X X. X ) /\ ( .- ` <. p , q >. ) e. u ) ) )
188 98 187 ax-mp 
 |-  ( <. p , q >. e. ( `' .- " u ) <-> ( <. p , q >. e. ( X X. X ) /\ ( .- ` <. p , q >. ) e. u ) )
189 188 simprbi 
 |-  ( <. p , q >. e. ( `' .- " u ) -> ( .- ` <. p , q >. ) e. u )
190 186 189 syl 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( .- ` <. p , q >. ) e. u )
191 182 190 eqeltrd 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) e. u )
192 53 54 syl 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) )
193 192 ad2antrr 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) )
194 elpreima 
 |-  ( ( -g ` H ) Fn ( ( Base ` H ) X. ( Base ` H ) ) -> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) e. u ) ) )
195 193 194 syl 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) <-> ( <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. ) e. u ) ) )
196 169 191 195 mpbir2and 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. [ p ] ( G ~QG Y ) , [ q ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) )
197 162 196 eqeltrd 
 |-  ( ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) /\ ( p e. c /\ q e. d ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) )
198 197 ralrimivva 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) )
199 opeq1 
 |-  ( z = ( F ` p ) -> <. z , w >. = <. ( F ` p ) , w >. )
200 199 eleq1d 
 |-  ( z = ( F ` p ) -> ( <. z , w >. e. ( `' ( -g ` H ) " u ) <-> <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
201 200 ralbidv 
 |-  ( z = ( F ` p ) -> ( A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
202 201 ralima 
 |-  ( ( F Fn X /\ c C_ X ) -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
203 79 202 mpan 
 |-  ( c C_ X -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) ) )
204 opeq2 
 |-  ( w = ( F ` q ) -> <. ( F ` p ) , w >. = <. ( F ` p ) , ( F ` q ) >. )
205 204 eleq1d 
 |-  ( w = ( F ` q ) -> ( <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
206 205 ralima 
 |-  ( ( F Fn X /\ d C_ X ) -> ( A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
207 79 206 mpan 
 |-  ( d C_ X -> ( A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
208 207 ralbidv 
 |-  ( d C_ X -> ( A. p e. c A. w e. ( F " d ) <. ( F ` p ) , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
209 203 208 sylan9bb 
 |-  ( ( c C_ X /\ d C_ X ) -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
210 136 147 209 syl2anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) <-> A. p e. c A. q e. d <. ( F ` p ) , ( F ` q ) >. e. ( `' ( -g ` H ) " u ) ) )
211 198 210 mpbird 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) )
212 dfss3 
 |-  ( ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) <-> A. y e. ( ( F " c ) X. ( F " d ) ) y e. ( `' ( -g ` H ) " u ) )
213 eleq1 
 |-  ( y = <. z , w >. -> ( y e. ( `' ( -g ` H ) " u ) <-> <. z , w >. e. ( `' ( -g ` H ) " u ) ) )
214 213 ralxp 
 |-  ( A. y e. ( ( F " c ) X. ( F " d ) ) y e. ( `' ( -g ` H ) " u ) <-> A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) )
215 212 214 bitri 
 |-  ( ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) <-> A. z e. ( F " c ) A. w e. ( F " d ) <. z , w >. e. ( `' ( -g ` H ) " u ) )
216 211 215 sylibr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) )
217 xpeq1 
 |-  ( r = ( F " c ) -> ( r X. s ) = ( ( F " c ) X. s ) )
218 217 eleq2d 
 |-  ( r = ( F " c ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) ) )
219 217 sseq1d 
 |-  ( r = ( F " c ) -> ( ( r X. s ) C_ ( `' ( -g ` H ) " u ) <-> ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) ) )
220 218 219 anbi12d 
 |-  ( r = ( F " c ) -> ( ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) /\ ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
221 xpeq2 
 |-  ( s = ( F " d ) -> ( ( F " c ) X. s ) = ( ( F " c ) X. ( F " d ) ) )
222 221 eleq2d 
 |-  ( s = ( F " d ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) ) )
223 221 sseq1d 
 |-  ( s = ( F " d ) -> ( ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) <-> ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) ) )
224 222 223 anbi12d 
 |-  ( s = ( F " d ) -> ( ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. s ) /\ ( ( F " c ) X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) /\ ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) ) ) )
225 220 224 rspc2ev 
 |-  ( ( ( F " c ) e. K /\ ( F " d ) e. K /\ ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( F " c ) X. ( F " d ) ) /\ ( ( F " c ) X. ( F " d ) ) C_ ( `' ( -g ` H ) " u ) ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
226 126 129 152 216 225 syl112anc 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( ( c e. J /\ d e. J ) /\ ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
227 226 expr 
 |-  ( ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) /\ ( c e. J /\ d e. J ) ) -> ( ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
228 227 rexlimdvva 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( E. c e. J E. d e. J ( ( a e. c /\ b e. d ) /\ ( c X. d ) C_ ( `' .- " u ) ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
229 121 228 syld 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( [ ( a ( -g ` G ) b ) ] ( G ~QG Y ) e. u -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
230 65 229 sylbid 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
231 230 adantld 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( ( Base ` H ) X. ( Base ` H ) ) /\ ( ( -g ` H ) ` <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. ) e. u ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
232 56 231 sylbid 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
233 opeq12 
 |-  ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> <. x , y >. = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. )
234 233 eleq1d 
 |-  ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) ) )
235 233 eleq1d 
 |-  ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) )
236 opex 
 |-  <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. _V
237 eleq1 
 |-  ( w = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. -> ( w e. ( r X. s ) <-> <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) ) )
238 237 anbi1d 
 |-  ( w = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. -> ( ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
239 238 2rexbidv 
 |-  ( w = <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. -> ( E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) <-> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
240 236 239 elab 
 |-  ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
241 235 240 bitrdi 
 |-  ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
242 234 241 imbi12d 
 |-  ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) <-> ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( `' ( -g ` H ) " u ) -> E. r e. K E. s e. K ( <. [ a ] ( G ~QG Y ) , [ b ] ( G ~QG Y ) >. e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) ) )
243 232 242 syl5ibrcom 
 |-  ( ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) /\ ( a e. X /\ b e. X ) ) -> ( ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
244 243 rexlimdvva 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( E. a e. X E. b e. X ( x = [ a ] ( G ~QG Y ) /\ y = [ b ] ( G ~QG Y ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
245 51 244 sylbird 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
246 245 com23 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> ( <. x , y >. e. ( ( Base ` H ) X. ( Base ` H ) ) -> <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) ) )
247 38 246 mpdd 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( <. x , y >. e. ( `' ( -g ` H ) " u ) -> <. x , y >. e. { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } ) )
248 37 247 relssdv 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( `' ( -g ` H ) " u ) C_ { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } )
249 ssabral 
 |-  ( ( `' ( -g ` H ) " u ) C_ { w | E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) } <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
250 248 249 sylib 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) )
251 eltx 
 |-  ( ( K e. ( TopOn ` ( Base ` H ) ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( ( `' ( -g ` H ) " u ) e. ( K tX K ) <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
252 24 24 251 syl2anc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( ( `' ( -g ` H ) " u ) e. ( K tX K ) <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
253 252 adantr 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( ( `' ( -g ` H ) " u ) e. ( K tX K ) <-> A. w e. ( `' ( -g ` H ) " u ) E. r e. K E. s e. K ( w e. ( r X. s ) /\ ( r X. s ) C_ ( `' ( -g ` H ) " u ) ) ) )
254 250 253 mpbird 
 |-  ( ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) /\ u e. K ) -> ( `' ( -g ` H ) " u ) e. ( K tX K ) )
255 254 ralrimiva 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> A. u e. K ( `' ( -g ` H ) " u ) e. ( K tX K ) )
256 txtopon 
 |-  ( ( K e. ( TopOn ` ( Base ` H ) ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( K tX K ) e. ( TopOn ` ( ( Base ` H ) X. ( Base ` H ) ) ) )
257 24 24 256 syl2anc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( K tX K ) e. ( TopOn ` ( ( Base ` H ) X. ( Base ` H ) ) ) )
258 iscn 
 |-  ( ( ( K tX K ) e. ( TopOn ` ( ( Base ` H ) X. ( Base ` H ) ) ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( ( -g ` H ) e. ( ( K tX K ) Cn K ) <-> ( ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) /\ A. u e. K ( `' ( -g ` H ) " u ) e. ( K tX K ) ) ) )
259 257 24 258 syl2anc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( ( -g ` H ) e. ( ( K tX K ) Cn K ) <-> ( ( -g ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) /\ A. u e. K ( `' ( -g ` H ) " u ) e. ( K tX K ) ) ) )
260 30 255 259 mpbir2and 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> ( -g ` H ) e. ( ( K tX K ) Cn K ) )
261 4 28 istgp2 
 |-  ( H e. TopGrp <-> ( H e. Grp /\ H e. TopSp /\ ( -g ` H ) e. ( ( K tX K ) Cn K ) ) )
262 8 27 260 261 syl3anbrc 
 |-  ( ( G e. TopGrp /\ Y e. ( NrmSGrp ` G ) ) -> H e. TopGrp )