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