Metamath Proof Explorer


Theorem tgrpset

Description: The translation group for a fiducial co-atom W . (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses tgrpset.h H = LHyp K
tgrpset.t T = LTrn K W
tgrpset.g G = TGrp K W
Assertion tgrpset K V W H G = Base ndx T + ndx f T , g T f g

Proof

Step Hyp Ref Expression
1 tgrpset.h H = LHyp K
2 tgrpset.t T = LTrn K W
3 tgrpset.g G = TGrp K W
4 1 tgrpfset K V TGrp K = w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g
5 4 fveq1d K V TGrp K W = w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g W
6 fveq2 w = W LTrn K w = LTrn K W
7 6 opeq2d w = W Base ndx LTrn K w = Base ndx LTrn K W
8 eqidd w = W f g = f g
9 6 6 8 mpoeq123dv w = W f LTrn K w , g LTrn K w f g = f LTrn K W , g LTrn K W f g
10 9 opeq2d w = W + ndx f LTrn K w , g LTrn K w f g = + ndx f LTrn K W , g LTrn K W f g
11 7 10 preq12d w = W Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
12 eqid w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g = w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g
13 prex Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g V
14 11 12 13 fvmpt W H w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g W = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
15 2 opeq2i Base ndx T = Base ndx LTrn K W
16 eqid f g = f g
17 2 2 16 mpoeq123i f T , g T f g = f LTrn K W , g LTrn K W f g
18 17 opeq2i + ndx f T , g T f g = + ndx f LTrn K W , g LTrn K W f g
19 15 18 preq12i Base ndx T + ndx f T , g T f g = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
20 14 19 eqtr4di W H w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g W = Base ndx T + ndx f T , g T f g
21 5 20 sylan9eq K V W H TGrp K W = Base ndx T + ndx f T , g T f g
22 3 21 syl5eq K V W H G = Base ndx T + ndx f T , g T f g