# Metamath Proof Explorer

## Theorem cdleml3N

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)$
cdleml3.o
Assertion cdleml3N

### 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 cdleml3.o
7 simp1
8 simp2
9 simp31
10 simp32
11 simp21
12 simp23
13 1 2 3 5 6 tendoid0
14 7 11 12 9 13 syl112anc
15 14 necon3bid
16 10 15 mpbird
17 simp33
18 simp22
19 1 2 3 5 6 tendoid0
20 7 18 12 9 19 syl112anc
21 20 necon3bid
22 17 21 mpbird
23 1 2 3 4 5 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)$
24 7 8 9 16 22 23 syl113anc
25 simpl1
26 simpr
27 simpl21
28 simpl23
29 2 3 5 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\in {E}\wedge {U}\in {E}\right)\wedge {f}\in {T}\right)\to \left({s}\circ {U}\right)\left({f}\right)={s}\left({U}\left({f}\right)\right)$
30 25 26 27 28 29 syl121anc
31 30 eqeq1d
32 simp11
33 simp2
34 simp121
35 2 5 tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\wedge {U}\in {E}\right)\to {s}\circ {U}\in {E}$
36 32 33 34 35 syl3anc
37 simp122
38 simp3
39 simp123
40 simp131
41 1 2 3 5 tendocan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({s}\circ {U}\in {E}\wedge {V}\in {E}\wedge \left({s}\circ {U}\right)\left({f}\right)={V}\left({f}\right)\right)\wedge \left({f}\in {T}\wedge {f}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {s}\circ {U}={V}$
42 32 36 37 38 39 40 41 syl132anc
43 42 3expia
44 31 43 sylbird
45 44 reximdva
46 24 45 mpd