| 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 ) |