# Metamath Proof Explorer

## Theorem tendoconid

Description: The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013)

Ref Expression
Hypotheses tendoid0.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
tendoid0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
tendoid0.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
tendoid0.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
tendoid0.o ${⊢}{O}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
Assertion tendoconid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\to {U}\circ {V}\ne {O}$

### Proof

Step Hyp Ref Expression
1 tendoid0.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 tendoid0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 tendoid0.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 tendoid0.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 tendoid0.o ${⊢}{O}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
6 1 2 3 cdlemftr0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \exists {g}\in {T}\phantom{\rule{.4em}{0ex}}{g}\ne {\mathrm{I}↾}_{{B}}$
7 6 3ad2ant1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\to \exists {g}\in {T}\phantom{\rule{.4em}{0ex}}{g}\ne {\mathrm{I}↾}_{{B}}$
8 simpl1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 simpl3l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\in {E}$
10 2 3 4 tendof ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\right)\to {V}:{T}⟶{T}$
11 8 9 10 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}:{T}⟶{T}$
12 simprl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {g}\in {T}$
13 fvco3 ${⊢}\left({V}:{T}⟶{T}\wedge {g}\in {T}\right)\to \left({U}\circ {V}\right)\left({g}\right)={U}\left({V}\left({g}\right)\right)$
14 11 12 13 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({U}\circ {V}\right)\left({g}\right)={U}\left({V}\left({g}\right)\right)$
15 simpl2r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\ne {O}$
16 simpl2l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\in {E}$
17 2 3 4 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\wedge {g}\in {T}\right)\to {V}\left({g}\right)\in {T}$
18 8 9 12 17 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\left({g}\right)\in {T}$
19 simpl3r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\ne {O}$
20 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)$
21 1 2 3 4 5 tendoid0 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({V}\left({g}\right)={\mathrm{I}↾}_{{B}}↔{V}={O}\right)$
22 8 9 20 21 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({V}\left({g}\right)={\mathrm{I}↾}_{{B}}↔{V}={O}\right)$
23 22 necon3bid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({V}\left({g}\right)\ne {\mathrm{I}↾}_{{B}}↔{V}\ne {O}\right)$
24 19 23 mpbird ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\left({g}\right)\ne {\mathrm{I}↾}_{{B}}$
25 1 2 3 4 5 tendoid0 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge \left({V}\left({g}\right)\in {T}\wedge {V}\left({g}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({U}\left({V}\left({g}\right)\right)={\mathrm{I}↾}_{{B}}↔{U}={O}\right)$
26 8 16 18 24 25 syl112anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({U}\left({V}\left({g}\right)\right)={\mathrm{I}↾}_{{B}}↔{U}={O}\right)$
27 26 necon3bid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({U}\left({V}\left({g}\right)\right)\ne {\mathrm{I}↾}_{{B}}↔{U}\ne {O}\right)$
28 15 27 mpbird ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\left({V}\left({g}\right)\right)\ne {\mathrm{I}↾}_{{B}}$
29 14 28 eqnetrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({U}\circ {V}\right)\left({g}\right)\ne {\mathrm{I}↾}_{{B}}$
30 2 4 tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge {V}\in {E}\right)\to {U}\circ {V}\in {E}$
31 8 16 9 30 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\circ {V}\in {E}$
32 1 2 3 4 5 tendoid0 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\circ {V}\in {E}\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left(\left({U}\circ {V}\right)\left({g}\right)={\mathrm{I}↾}_{{B}}↔{U}\circ {V}={O}\right)$
33 8 31 20 32 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left(\left({U}\circ {V}\right)\left({g}\right)={\mathrm{I}↾}_{{B}}↔{U}\circ {V}={O}\right)$
34 33 necon3bid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left(\left({U}\circ {V}\right)\left({g}\right)\ne {\mathrm{I}↾}_{{B}}↔{U}\circ {V}\ne {O}\right)$
35 29 34 mpbid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\wedge \left({g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\circ {V}\ne {O}$
36 7 35 rexlimddv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {U}\ne {O}\right)\wedge \left({V}\in {E}\wedge {V}\ne {O}\right)\right)\to {U}\circ {V}\ne {O}$