Metamath Proof Explorer


Theorem tgrpfset

Description: The translation group maps for a lattice K . (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypothesis tgrpset.h H = LHyp K
Assertion tgrpfset K V TGrp K = w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g

Proof

Step Hyp Ref Expression
1 tgrpset.h H = LHyp K
2 elex K V K V
3 fveq2 k = K LHyp k = LHyp K
4 3 1 eqtr4di k = K LHyp k = H
5 fveq2 k = K LTrn k = LTrn K
6 5 fveq1d k = K LTrn k w = LTrn K w
7 6 opeq2d k = K Base ndx LTrn k w = Base ndx LTrn K w
8 eqidd k = K f g = f g
9 6 6 8 mpoeq123dv k = K f LTrn k w , g LTrn k w f g = f LTrn K w , g LTrn K w f g
10 9 opeq2d k = K + 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 k = K 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 4 11 mpteq12dv k = K w LHyp k 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 df-tgrp TGrp = k V w LHyp k Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g
14 12 13 1 mptfvmpt K V TGrp K = w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g
15 2 14 syl K V TGrp K = w H Base ndx LTrn K w + ndx f LTrn K w , g LTrn K w f g