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 X = Base G
eqgval.n N = inv g G
eqgval.p + ˙ = + G
eqgval.r R = G ~ QG S
Assertion eqgfval G V S X R = x y | x y X N x + ˙ y S

Proof

Step Hyp Ref Expression
1 eqgval.x X = Base G
2 eqgval.n N = inv g G
3 eqgval.p + ˙ = + G
4 eqgval.r R = G ~ QG S
5 elex G V G V
6 1 fvexi X V
7 6 ssex S X S V
8 simpl g = G s = S g = G
9 8 fveq2d g = G s = S Base g = Base G
10 9 1 eqtr4di g = G s = S Base g = X
11 10 sseq2d g = G s = S x y Base g x y X
12 8 fveq2d g = G s = S + g = + G
13 12 3 eqtr4di g = G s = S + g = + ˙
14 8 fveq2d g = G s = S inv g g = inv g G
15 14 2 eqtr4di g = G s = S inv g g = N
16 15 fveq1d g = G s = S inv g g x = N x
17 eqidd g = G s = S y = y
18 13 16 17 oveq123d g = G s = S inv g g x + g y = N x + ˙ y
19 simpr g = G s = S s = S
20 18 19 eleq12d g = G s = S inv g g x + g y s N x + ˙ y S
21 11 20 anbi12d g = G s = S x y Base g inv g g x + g y s x y X N x + ˙ y S
22 21 opabbidv g = G s = S x y | x y Base g inv g g x + g y s = x y | x y X N x + ˙ y S
23 df-eqg ~ QG = g V , s V x y | x y Base g inv g g x + g y s
24 6 6 xpex X × X V
25 simpl x y X N x + ˙ y S x y X
26 vex x V
27 vex y V
28 26 27 prss x X y X x y X
29 25 28 sylibr x y X N x + ˙ y S x X y X
30 29 ssopab2i x y | x y X N x + ˙ y S x y | x X y X
31 df-xp X × X = x y | x X y X
32 30 31 sseqtrri x y | x y X N x + ˙ y S X × X
33 24 32 ssexi x y | x y X N x + ˙ y S V
34 22 23 33 ovmpoa G V S V G ~ QG S = x y | x y X N x + ˙ y S
35 4 34 syl5eq G V S V R = x y | x y X N x + ˙ y S
36 5 7 35 syl2an G V S X R = x y | x y X N x + ˙ y S