Metamath Proof Explorer

Theorem tendoipl

Description: Property 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 ⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
tendoi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoi.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
tendoi.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendoipl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) = 𝑂 )

Proof

Step Hyp Ref Expression
1 tendoicl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendoicl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendoicl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendoicl.i ⊢ 𝐼 = ( 𝑠 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ◡ ( 𝑠 ‘ 𝑓 ) ) )
5 tendoi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
6 tendoi.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
7 tendoi.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 1 2 3 4 tendoicl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝐼 ‘ 𝑆 ) ∈ 𝐸 )
10 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → 𝑆 ∈ 𝐸 )
11 1 2 3 6 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ 𝑆 ) ∈ 𝐸 ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ∈ 𝐸 )
12 8 9 10 11 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ∈ 𝐸 )
13 5 1 2 3 7 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
14 13 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → 𝑂 ∈ 𝐸 )
15 4 2 tendoi2 ⊢ ( ( 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝑔 ) )
16 15 adantll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) = ◡ ( 𝑆 ‘ 𝑔 ) )
17 16 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( ◡ ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
18 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 )
20 19 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 )
21 5 1 2 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝑔 ) ∈ 𝑇 ) → ( 𝑆 ‘ 𝑔 ) : 𝐵 –1-1-onto→ 𝐵 )
22 18 20 21 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑆 ‘ 𝑔 ) : 𝐵 –1-1-onto→ 𝐵 )
23 f1ococnv1 ⊢ ( ( 𝑆 ‘ 𝑔 ) : 𝐵 –1-1-onto→ 𝐵 → ( ◡ ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) )
24 22 23 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ◡ ( 𝑆 ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) )
25 17 24 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) )
26 9 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝐼 ‘ 𝑆 ) ∈ 𝐸 )
27 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → 𝑆 ∈ 𝐸 )
28 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → 𝑔 ∈ 𝑇 )
29 6 2 tendopl2 ⊢ ( ( ( 𝐼 ‘ 𝑆 ) ∈ 𝐸 ∧ 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ‘ 𝑔 ) = ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
30 26 27 28 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ‘ 𝑔 ) = ( ( ( 𝐼 ‘ 𝑆 ) ‘ 𝑔 ) ∘ ( 𝑆 ‘ 𝑔 ) ) )
31 7 5 tendo02 ⊢ ( 𝑔 ∈ 𝑇 → ( 𝑂 ‘ 𝑔 ) = ( I ↾ 𝐵 ) )
32 31 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑂 ‘ 𝑔 ) = ( I ↾ 𝐵 ) )
33 25 30 32 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) )
34 33 ralrimiva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ∀ 𝑔 ∈ 𝑇 ( ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) )
35 1 2 3 tendoeq1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ∈ 𝐸 ∧ 𝑂 ∈ 𝐸 ) ∧ ∀ 𝑔 ∈ 𝑇 ( ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) ) → ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) = 𝑂 )
36 8 12 14 34 35 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐼 ‘ 𝑆 ) 𝑃 𝑆 ) = 𝑂 )