Metamath Proof Explorer


Theorem tendofset

Description: The set of all trace-preserving endomorphisms on the set of translations for a lattice K . (Contributed by NM, 8-Jun-2013)

Ref Expression
Hypotheses tendoset.l ˙ = K
tendoset.h H = LHyp K
Assertion tendofset K V TEndo K = w H s | s : LTrn K w LTrn K w f LTrn K w g LTrn K w s f g = s f s g f LTrn K w trL K w s f ˙ trL K w f

Proof

Step Hyp Ref Expression
1 tendoset.l ˙ = K
2 tendoset.h H = LHyp K
3 elex K V K V
4 fveq2 k = K LHyp k = LHyp K
5 4 2 eqtr4di k = K LHyp k = H
6 fveq2 k = K LTrn k = LTrn K
7 6 fveq1d k = K LTrn k w = LTrn K w
8 7 7 feq23d k = K s : LTrn k w LTrn k w s : LTrn K w LTrn K w
9 7 raleqdv k = K g LTrn k w s f g = s f s g g LTrn K w s f g = s f s g
10 7 9 raleqbidv k = K f LTrn k w g LTrn k w s f g = s f s g f LTrn K w g LTrn K w s f g = s f s g
11 fveq2 k = K trL k = trL K
12 11 fveq1d k = K trL k w = trL K w
13 12 fveq1d k = K trL k w s f = trL K w s f
14 fveq2 k = K k = K
15 14 1 eqtr4di k = K k = ˙
16 12 fveq1d k = K trL k w f = trL K w f
17 13 15 16 breq123d k = K trL k w s f k trL k w f trL K w s f ˙ trL K w f
18 7 17 raleqbidv k = K f LTrn k w trL k w s f k trL k w f f LTrn K w trL K w s f ˙ trL K w f
19 8 10 18 3anbi123d k = K s : LTrn k w LTrn k w f LTrn k w g LTrn k w s f g = s f s g f LTrn k w trL k w s f k trL k w f s : LTrn K w LTrn K w f LTrn K w g LTrn K w s f g = s f s g f LTrn K w trL K w s f ˙ trL K w f
20 19 abbidv k = K s | s : LTrn k w LTrn k w f LTrn k w g LTrn k w s f g = s f s g f LTrn k w trL k w s f k trL k w f = s | s : LTrn K w LTrn K w f LTrn K w g LTrn K w s f g = s f s g f LTrn K w trL K w s f ˙ trL K w f
21 5 20 mpteq12dv k = K w LHyp k s | s : LTrn k w LTrn k w f LTrn k w g LTrn k w s f g = s f s g f LTrn k w trL k w s f k trL k w f = w H s | s : LTrn K w LTrn K w f LTrn K w g LTrn K w s f g = s f s g f LTrn K w trL K w s f ˙ trL K w f
22 df-tendo TEndo = k V w LHyp k s | s : LTrn k w LTrn k w f LTrn k w g LTrn k w s f g = s f s g f LTrn k w trL k w s f k trL k w f
23 21 22 2 mptfvmpt K V TEndo K = w H s | s : LTrn K w LTrn K w f LTrn K w g LTrn K w s f g = s f s g f LTrn K w trL K w s f ˙ trL K w f
24 3 23 syl K V TEndo K = w H s | s : LTrn K w LTrn K w f LTrn K w g LTrn K w s f g = s f s g f LTrn K w trL K w s f ˙ trL K w f