Metamath Proof Explorer

Theorem tendoicl

Description: Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013)

Ref Expression
Hypotheses tendoicl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoicl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoicl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoicl.i ⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
Assertion tendoicl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐼 ‘ 𝑆 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 tendoicl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendoicl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendoicl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendoicl.i ⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 )
10 9 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 )
11 1 2 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 )
12 8 10 11 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 )
13 12 fmpttd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) : 𝑇 ⟶ 𝑇 )
14 4 2 tendoi ⊢ ( 𝑆 ∈ 𝐸 → ( 𝐼 ‘ 𝑆 ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )
15 14 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐼 ‘ 𝑆 ) = ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) )
16 15 feq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐼 ‘ 𝑆 ) : 𝑇 ⟶ 𝑇 ↔ ( 𝑔 ∈ 𝑇 ↦ ◡ ( 𝑆 ‘ 𝑔 ) ) : 𝑇 ⟶ 𝑇 ) )
17 13 16 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐼 ‘ 𝑆 ) : 𝑇 ⟶ 𝑇 )
18 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → 𝑆 ∈ 𝐸 )
19 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑔 ∘ ℎ ) ∈ 𝑇 )
20 19 3adant1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑔 ∘ ℎ ) ∈ 𝑇 )
21 4 2 tendoi2 ⊢ ( ( 𝑆 ∈ 𝐸 ∧ ( 𝑔 ∘ ℎ ) ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ ( 𝑔 ∘ ℎ ) ) = ◡ ( 𝑆 ‘ ( 𝑔 ∘ ℎ ) ) )
22 18 20 21 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ ( 𝑔 ∘ ℎ ) ) = ◡ ( 𝑆 ‘ ( 𝑔 ∘ ℎ ) ) )
23 cnvco ⊢ ◡ ( ( 𝑆 ‘ ℎ ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( ◡ ( 𝑆 ‘ 𝑔 ) ∘ ◡ ( 𝑆 ‘ ℎ ) )
24 1 2 ltrncom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑔 ∘ ℎ ) = ( ℎ ∘ 𝑔 ) )
25 24 3adant1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑔 ∘ ℎ ) = ( ℎ ∘ 𝑔 ) )
26 25 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝑔 ∘ ℎ ) ) = ( 𝑆 ‘ ( ℎ ∘ 𝑔 ) ) )
27 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → 𝐾 ∈ HL )
28 simp1lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → 𝑊 ∈ 𝐻 )
29 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ℎ ∈ 𝑇 )
30 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → 𝑔 ∈ 𝑇 )
31 1 2 3 tendovalco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸 ) ∧ ( ℎ ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( ℎ ∘ 𝑔 ) ) = ( ( 𝑆 ‘ ℎ ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
32 27 28 18 29 30 31 syl32anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑆 ‘ ( ℎ ∘ 𝑔 ) ) = ( ( 𝑆 ‘ ℎ ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
33 26 32 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝑔 ∘ ℎ ) ) = ( ( 𝑆 ‘ ℎ ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
34 33 cnveqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ◡ ( 𝑆 ‘ ( 𝑔 ∘ ℎ ) ) = ◡ ( ( 𝑆 ‘ ℎ ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
35 4 2 tendoi2 ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝑔 ) )
36 18 30 35 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝑔 ) )
37 4 2 tendoi2 ⊢ ( ( 𝑆 ∈ 𝐸 ∧ ℎ ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ ℎ ) = ◡ ( 𝑆 ‘ ℎ ) )
38 18 29 37 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ ℎ ) = ◡ ( 𝑆 ‘ ℎ ) )
39 36 38 coeq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( ( 𝐼 ‘ 𝑆 ) ‘ ℎ ) ) = ( ◡ ( 𝑆 ‘ 𝑔 ) ∘ ◡ ( 𝑆 ‘ ℎ ) ) )
40 23 34 39 3eqtr4a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ◡ ( 𝑆 ‘ ( 𝑔 ∘ ℎ ) ) = ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( ( 𝐼 ‘ 𝑆 ) ‘ ℎ ) ) )
41 22 40 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ ( 𝑔 ∘ ℎ ) ) = ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( ( 𝐼 ‘ 𝑆 ) ‘ ℎ ) ) )
42 35 adantll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝑔 ) )
43 42 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ◡ ( 𝑆 ‘ 𝑔 ) ) )
44 1 2 6 trlcnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ◡ ( 𝑆 ‘ 𝑔 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑔 ) ) )
45 8 10 44 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ◡ ( 𝑆 ‘ 𝑔 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑔 ) ) )
46 43 45 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑔 ) ) )
47 5 1 2 6 3 tendotp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑔 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) )
48 47 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑔 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) )
49 46 48 eqbrtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) )
50 5 1 2 6 3 7 17 41 49 istendod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐼 ‘ 𝑆 ) ∈ 𝐸 )