This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } )
36 5 7 35 syl2an ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } )