# Metamath Proof Explorer

## Theorem cdleml1N

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 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)$

### 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 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
10 9 2 3 4 5 tendotp ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\in {E}\wedge {f}\in {T}\right)\to {R}\left({U}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)$
11 6 7 8 10 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 {R}\left({U}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)$
12 simp1l ${⊢}\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 {K}\in \mathrm{HL}$
13 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
14 12 13 syl ${⊢}\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 {K}\in \mathrm{AtLat}$
15 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}$
16 6 7 8 15 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}$
17 simp32 ${⊢}\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)\ne {\mathrm{I}↾}_{{B}}$
18 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
19 1 18 2 3 4 trlnidat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {U}\left({f}\right)\in {T}\wedge {U}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\to {R}\left({U}\left({f}\right)\right)\in \mathrm{Atoms}\left({K}\right)$
20 6 16 17 19 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 {R}\left({U}\left({f}\right)\right)\in \mathrm{Atoms}\left({K}\right)$
21 simp31 ${⊢}\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}\ne {\mathrm{I}↾}_{{B}}$
22 1 18 2 3 4 trlnidat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\wedge {f}\ne {\mathrm{I}↾}_{{B}}\right)\to {R}\left({f}\right)\in \mathrm{Atoms}\left({K}\right)$
23 6 8 21 22 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 {R}\left({f}\right)\in \mathrm{Atoms}\left({K}\right)$
24 9 18 atcmp ${⊢}\left({K}\in \mathrm{AtLat}\wedge {R}\left({U}\left({f}\right)\right)\in \mathrm{Atoms}\left({K}\right)\wedge {R}\left({f}\right)\in \mathrm{Atoms}\left({K}\right)\right)\to \left({R}\left({U}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)↔{R}\left({U}\left({f}\right)\right)={R}\left({f}\right)\right)$
25 14 20 23 24 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 \left({R}\left({U}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)↔{R}\left({U}\left({f}\right)\right)={R}\left({f}\right)\right)$
26 11 25 mpbid ${⊢}\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({f}\right)$
27 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}$
28 9 2 3 4 5 tendotp ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\in {E}\wedge {f}\in {T}\right)\to {R}\left({V}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)$
29 6 27 8 28 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 {R}\left({V}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)$
30 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}$
31 6 27 8 30 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}$
32 simp33 ${⊢}\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)\ne {\mathrm{I}↾}_{{B}}$
33 1 18 2 3 4 trlnidat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {V}\left({f}\right)\in {T}\wedge {V}\left({f}\right)\ne {\mathrm{I}↾}_{{B}}\right)\to {R}\left({V}\left({f}\right)\right)\in \mathrm{Atoms}\left({K}\right)$
34 6 31 32 33 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 {R}\left({V}\left({f}\right)\right)\in \mathrm{Atoms}\left({K}\right)$
35 9 18 atcmp ${⊢}\left({K}\in \mathrm{AtLat}\wedge {R}\left({V}\left({f}\right)\right)\in \mathrm{Atoms}\left({K}\right)\wedge {R}\left({f}\right)\in \mathrm{Atoms}\left({K}\right)\right)\to \left({R}\left({V}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)↔{R}\left({V}\left({f}\right)\right)={R}\left({f}\right)\right)$
36 14 34 23 35 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 \left({R}\left({V}\left({f}\right)\right){\le }_{{K}}{R}\left({f}\right)↔{R}\left({V}\left({f}\right)\right)={R}\left({f}\right)\right)$
37 29 36 mpbid ${⊢}\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({V}\left({f}\right)\right)={R}\left({f}\right)$
38 26 37 eqtr4d ${⊢}\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)$