Step |
Hyp |
Ref |
Expression |
1 |
|
eqgval.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
eqgval.n |
⊢ 𝑁 = ( invg ‘ 𝐺 ) |
3 |
|
eqgval.p |
⊢ + = ( +g ‘ 𝐺 ) |
4 |
|
eqgval.r |
⊢ 𝑅 = ( 𝐺 ~QG 𝑆 ) |
5 |
|
elex |
⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V ) |
6 |
1
|
fvexi |
⊢ 𝑋 ∈ V |
7 |
6
|
ssex |
⊢ ( 𝑆 ⊆ 𝑋 → 𝑆 ∈ V ) |
8 |
|
simpl |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → 𝑔 = 𝐺 ) |
9 |
8
|
fveq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) ) |
10 |
9 1
|
eqtr4di |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑔 ) = 𝑋 ) |
11 |
10
|
sseq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑔 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑋 ) ) |
12 |
8
|
fveq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) ) |
13 |
12 3
|
eqtr4di |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( +g ‘ 𝑔 ) = + ) |
14 |
8
|
fveq2d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( invg ‘ 𝑔 ) = ( invg ‘ 𝐺 ) ) |
15 |
14 2
|
eqtr4di |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( invg ‘ 𝑔 ) = 𝑁 ) |
16 |
15
|
fveq1d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) ) |
17 |
|
eqidd |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → 𝑦 = 𝑦 ) |
18 |
13 16 17
|
oveq123d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) ( +g ‘ 𝑔 ) 𝑦 ) = ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ) |
19 |
|
simpr |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 ) |
20 |
18 19
|
eleq12d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( ( ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) ( +g ‘ 𝑔 ) 𝑦 ) ∈ 𝑠 ↔ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) ) |
21 |
11 20
|
anbi12d |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑔 ) ∧ ( ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) ( +g ‘ 𝑔 ) 𝑦 ) ∈ 𝑠 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) ) ) |
22 |
21
|
opabbidv |
⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑔 ) ∧ ( ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) ( +g ‘ 𝑔 ) 𝑦 ) ∈ 𝑠 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ) |
23 |
|
df-eqg |
⊢ ~QG = ( 𝑔 ∈ V , 𝑠 ∈ V ↦ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑔 ) ∧ ( ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) ( +g ‘ 𝑔 ) 𝑦 ) ∈ 𝑠 ) } ) |
24 |
6 6
|
xpex |
⊢ ( 𝑋 × 𝑋 ) ∈ V |
25 |
|
simpl |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) → { 𝑥 , 𝑦 } ⊆ 𝑋 ) |
26 |
|
vex |
⊢ 𝑥 ∈ V |
27 |
|
vex |
⊢ 𝑦 ∈ V |
28 |
26 27
|
prss |
⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑋 ) |
29 |
25 28
|
sylibr |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) |
30 |
29
|
ssopab2i |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) } |
31 |
|
df-xp |
⊢ ( 𝑋 × 𝑋 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) } |
32 |
30 31
|
sseqtrri |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ⊆ ( 𝑋 × 𝑋 ) |
33 |
24 32
|
ssexi |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ∈ V |
34 |
22 23 33
|
ovmpoa |
⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐺 ~QG 𝑆 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ) |
35 |
4 34
|
syl5eq |
⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ) |
36 |
5 7 35
|
syl2an |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } ) |