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