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 = ( le ‘ 𝐾 )
tendoset.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion tendofset ( 𝐾𝑉 → ( TEndo ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )

Proof

Step Hyp Ref Expression
1 tendoset.l = ( le ‘ 𝐾 )
2 tendoset.h 𝐻 = ( LHyp ‘ 𝐾 )
3 elex ( 𝐾𝑉𝐾 ∈ V )
4 fveq2 ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
5 4 2 eqtr4di ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
6 fveq2 ( 𝑘 = 𝐾 → ( LTrn ‘ 𝑘 ) = ( LTrn ‘ 𝐾 ) )
7 6 fveq1d ( 𝑘 = 𝐾 → ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) )
8 7 7 feq23d ( 𝑘 = 𝐾 → ( 𝑠 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↔ 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) )
9 7 raleqdv ( 𝑘 = 𝐾 → ( ∀ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ↔ ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ) )
10 7 9 raleqbidv ( 𝑘 = 𝐾 → ( ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ) )
11 fveq2 ( 𝑘 = 𝐾 → ( trL ‘ 𝑘 ) = ( trL ‘ 𝐾 ) )
12 11 fveq1d ( 𝑘 = 𝐾 → ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) )
13 12 fveq1d ( 𝑘 = 𝐾 → ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) )
14 fveq2 ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
15 14 1 eqtr4di ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = )
16 12 fveq1d ( 𝑘 = 𝐾 → ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) )
17 13 15 16 breq123d ( 𝑘 = 𝐾 → ( ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) )
18 7 17 raleqbidv ( 𝑘 = 𝐾 → ( ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ↔ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) )
19 8 10 18 3anbi123d ( 𝑘 = 𝐾 → ( ( 𝑠 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ) ↔ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) ) )
20 19 abbidv ( 𝑘 = 𝐾 → { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } = { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } )
21 5 20 mpteq12dv ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) = ( 𝑤𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )
22 df-tendo TEndo = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( le ‘ 𝑘 ) ( ( ( trL ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )
23 21 22 2 mptfvmpt ( 𝐾 ∈ V → ( TEndo ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )
24 3 23 syl ( 𝐾𝑉 → ( TEndo ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑠 ∣ ( 𝑠 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ∀ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( 𝑠 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑠𝑓 ) ∘ ( 𝑠𝑔 ) ) ∧ ∀ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( 𝑠𝑓 ) ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )