Metamath Proof Explorer


Theorem eqgfval

Description: Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses eqgval.x 𝑋 = ( Base ‘ 𝐺 )
eqgval.n 𝑁 = ( invg𝐺 )
eqgval.p + = ( +g𝐺 )
eqgval.r 𝑅 = ( 𝐺 ~QG 𝑆 )
Assertion eqgfval ( ( 𝐺𝑉𝑆𝑋 ) → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁𝑥 ) + 𝑦 ) ∈ 𝑆 ) } )

Proof

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 ( ( 𝐺𝑉𝑆𝑋 ) → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁𝑥 ) + 𝑦 ) ∈ 𝑆 ) } )