# Metamath Proof Explorer

## Theorem cdleml2N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleml1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdleml1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleml1.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdleml1.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdleml1.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion cdleml2N ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{s}\left({U}\left({f}\right)\right)={V}\left({f}\right)$

### Proof

Step Hyp Ref Expression
1 cdleml1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdleml1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 cdleml1.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 cdleml1.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
5 cdleml1.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
6 simp1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 simp21 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\in {E}$
8 simp23 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {f}\in {T}$
9 2 3 5 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge {f}\in {T}\right)\to {U}\left({f}\right)\in {T}$
10 6 7 8 9 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\left({f}\right)\in {T}$
11 simp22 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\in {E}$
12 2 3 5 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\wedge {f}\in {T}\right)\to {V}\left({f}\right)\in {T}$
13 6 11 8 12 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\left({f}\right)\in {T}$
14 1 2 3 4 5 cdleml1N ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {R}\left({U}\left({f}\right)\right)={R}\left({V}\left({f}\right)\right)$
15 2 3 4 5 cdlemk ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\left({f}\right)\in {T}\wedge {V}\left({f}\right)\in {T}\right)\wedge {R}\left({U}\left({f}\right)\right)={R}\left({V}\left({f}\right)\right)\right)\to \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{s}\left({U}\left({f}\right)\right)={V}\left({f}\right)$
16 6 10 13 14 15 syl121anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {f}\in {T}\right)\wedge \left({f}\ne {\mathrm{I}↾}_{{B}}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \exists {s}\in {E}\phantom{\rule{.4em}{0ex}}{s}\left({U}\left({f}\right)\right)={V}\left({f}\right)$