Theorem eqgval

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

	Ref	Expression
Hypotheses	eqgval.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	eqgval.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	eqgval.p	⊢ + = ( +g ‘ 𝐺 )
	eqgval.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
Assertion	eqgval	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqgval.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		eqgval.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
3		eqgval.p	⊢ + = ( +g ‘ 𝐺 )
4		eqgval.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
5	1 2 3 4	eqgfval	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } )
6	5	breqd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } 𝐵 ) )
7		brabv	⊢ ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
8	7	adantl	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
9		simpr1	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) → 𝐴 ∈ 𝑋 )
10	9	elexd	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) → 𝐴 ∈ V )
11		simpr2	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) → 𝐵 ∈ 𝑋 )
12	11	elexd	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) → 𝐵 ∈ V )
13	10 12	jca	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
14		vex	⊢ 𝑥 ∈ V
15		vex	⊢ 𝑦 ∈ V
16	14 15	prss	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑋 )
17		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑋 ↔ 𝐴 ∈ 𝑋 ) )
18		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋 ) )
19	17 18	bi2anan9	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) )
20	16 19	bitr3id	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( { 𝑥 , 𝑦 } ⊆ 𝑋 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) )
21		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝐴 ) )
22		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
23	21 22	oveqan12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) = ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) )
24	23	eleq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ↔ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) )
25	20 24	anbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) )
26		df-3an	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) )
27	25 26	bitr4di	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) )
28		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) }
29	27 28	brabga	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) )
30	8 13 29	pm5.21nd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑋 ∧ ( ( 𝑁 ‘ 𝑥 ) + 𝑦 ) ∈ 𝑆 ) } 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) )
31	6 30	bitrd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝑁 ‘ 𝐴 ) + 𝐵 ) ∈ 𝑆 ) ) )