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=BaseK
cdleml6.j ⊢∨˙=join⁡K
cdleml6.m ⊢∧˙=meet⁡K
cdleml6.h ⊢H=LHyp⁡K
cdleml6.t ⊢T=LTrn⁡K⁡W
cdleml6.r ⊢R=trL⁡K⁡W
cdleml6.p ⊢Q=oc⁡K⁡W
cdleml6.z ⊢Z=Q∨˙R⁡b∧˙h⁡Q∨˙R⁡b∘s⁡h-1
cdleml6.y ⊢Y=Q∨˙R⁡g∧˙Z∨˙R⁡g∘b-1
cdleml6.x ⊢X=ιz∈T|∀b∈Tb≠I↾B∧R⁡b≠R⁡s⁡h∧R⁡b≠R⁡g→z⁡Q=Y
cdleml6.u ⊢U=g∈T⟼ifs⁡h=hgX
cdleml6.e ⊢E=TEndo⁡K⁡W
cdleml6.o ⊢0˙=f∈T⟼I↾B
Assertion cdleml7 ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U∘s⁡h=I↾T⁡h

Proof

Step Hyp Ref Expression
1 cdleml6.b ⊢B=BaseK
2 cdleml6.j ⊢∨˙=join⁡K
3 cdleml6.m ⊢∧˙=meet⁡K
4 cdleml6.h ⊢H=LHyp⁡K
5 cdleml6.t ⊢T=LTrn⁡K⁡W
6 cdleml6.r ⊢R=trL⁡K⁡W
7 cdleml6.p ⊢Q=oc⁡K⁡W
8 cdleml6.z ⊢Z=Q∨˙R⁡b∧˙h⁡Q∨˙R⁡b∘s⁡h-1
9 cdleml6.y ⊢Y=Q∨˙R⁡g∧˙Z∨˙R⁡g∘b-1
10 cdleml6.x ⊢X=ιz∈T|∀b∈Tb≠I↾B∧R⁡b≠R⁡s⁡h∧R⁡b≠R⁡g→z⁡Q=Y
11 cdleml6.u ⊢U=g∈T⟼ifs⁡h=hgX
12 cdleml6.e ⊢E=TEndo⁡K⁡W
13 cdleml6.o ⊢0˙=f∈T⟼I↾B
14 1 2 3 4 5 6 7 8 9 10 11 12 13 cdleml6 ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U∈E∧U⁡s⁡h=h
15 14 simprd ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U⁡s⁡h=h
16 simp1 ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→K∈HL∧W∈H
17 14 simpld ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U∈E
18 simp3l ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→s∈E
19 simp2 ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→h∈T
20 4 5 12 tendocoval ⊢K∈HL∧W∈H∧U∈E∧s∈E∧h∈T→U∘s⁡h=U⁡s⁡h
21 16 17 18 19 20 syl121anc ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U∘s⁡h=U⁡s⁡h
22 fvresi ⊢h∈T→I↾T⁡h=h
23 22 3ad2ant2 ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→I↾T⁡h=h
24 15 21 23 3eqtr4d ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U∘s⁡h=I↾T⁡h