This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑓 ) ) } ) )