Theorem eqgval 19195

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

Hypotheses

Ref	Expression
eqgval.x	⊢ 𝑋 = (Base‘𝐺)
eqgval.n	⊢ 𝑁 = (invg‘𝐺)
eqgval.p	⊢ + = (+g‘𝐺)
eqgval.r	⊢ 𝑅 = (𝐺 ~QG 𝑆)

Assertion

Ref	Expression
eqgval	⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)))

Proof of Theorem eqgval

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  {cpr 4628   class class class wbr 5143  {copab 5205  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  inv_gcminusg 18952   ~_QG cqg 19140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-eqg 19143

This theorem is referenced by:  eqger  19196  eqglact  19197  eqgid  19198  eqgcpbl  19200  ghmqusnsglem1  19298  ghmquskerlem1  19301  gastacos  19328  orbstafun  19329  sylow2blem1  19638  sylow2blem3  19640  eqgabl  19852  tgpconncompeqg  24120  tgpconncomp  24121  qustgpopn  24128  qusker  33377  eqgvscpbl  33378  qusxpid  33391  nsgqusf1olem3  33443  qsnzr  33483  qsdrngilem  33522  qsdrnglem2  33524