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 ∧ 𝑊𝐻 ) ∧ 𝑆𝐸 ) → ( 𝑂 𝑃 𝑆 ) = 𝑆 )