# Metamath Proof Explorer

## Theorem cdleml7

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013)

Ref Expression
Hypotheses cdleml6.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdleml6.j
cdleml6.m
cdleml6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleml6.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdleml6.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdleml6.p ${⊢}{Q}=\mathrm{oc}\left({K}\right)\left({W}\right)$
cdleml6.z
cdleml6.y
cdleml6.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({s}\left({h}\right)\right)\wedge {R}\left({b}\right)\ne {R}\left({g}\right)\right)\to {z}\left({Q}\right)={Y}\right)\right)$
cdleml6.u ${⊢}{U}=\left({g}\in {T}⟼if\left({s}\left({h}\right)={h},{g},{X}\right)\right)$
cdleml6.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
cdleml6.o
Assertion cdleml7

### Proof

Step Hyp Ref Expression
1 cdleml6.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdleml6.j
3 cdleml6.m
4 cdleml6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
5 cdleml6.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 cdleml6.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
7 cdleml6.p ${⊢}{Q}=\mathrm{oc}\left({K}\right)\left({W}\right)$
8 cdleml6.z
9 cdleml6.y
10 cdleml6.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({s}\left({h}\right)\right)\wedge {R}\left({b}\right)\ne {R}\left({g}\right)\right)\to {z}\left({Q}\right)={Y}\right)\right)$
11 cdleml6.u ${⊢}{U}=\left({g}\in {T}⟼if\left({s}\left({h}\right)={h},{g},{X}\right)\right)$
12 cdleml6.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
13 cdleml6.o
14 1 2 3 4 5 6 7 8 9 10 11 12 13 cdleml6
15 14 simprd
16 simp1
17 14 simpld
18 simp3l
19 simp2
20 4 5 12 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {s}\in {E}\right)\wedge {h}\in {T}\right)\to \left({U}\circ {s}\right)\left({h}\right)={U}\left({s}\left({h}\right)\right)$
21 16 17 18 19 20 syl121anc
22 fvresi ${⊢}{h}\in {T}\to \left({\mathrm{I}↾}_{{T}}\right)\left({h}\right)={h}$