Metamath Proof Explorer

Theorem tendo0pl

Description: Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013)

Ref Expression
Hypotheses tendo0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendo0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendo0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendo0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendo0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
tendo0pl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
Assertion tendo0pl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑂 𝑃 𝑆 ) = 𝑆 )

Proof

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