Metamath Proof Explorer

Theorem cdleml8

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 cdleml8 ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→U∘s=I↾T

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 simp1 ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→K∈HL∧W∈H
15 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
16 15 3adant2r ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→U∈E∧U⁡s⁡h=h
17 16 simpld ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→U∈E
18 simp3l ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→s∈E
19 4 12 tendococl ⊢K∈HL∧W∈H∧U∈E∧s∈E→U∘s∈E
20 14 17 18 19 syl3anc ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→U∘s∈E
21 4 5 12 tendoidcl ⊢K∈HL∧W∈H→I↾T∈E
22 21 3ad2ant1 ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→I↾T∈E
23 1 2 3 4 5 6 7 8 9 10 11 12 13 cdleml7 ⊢K∈HL∧W∈H∧h∈T∧s∈E∧s≠0˙→U∘s⁡h=I↾T⁡h
24 23 3adant2r ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→U∘s⁡h=I↾T⁡h
25 simp2 ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→h∈T∧h≠I↾B
26 1 4 5 12 tendocan ⊢K∈HL∧W∈H∧U∘s∈E∧I↾T∈E∧U∘s⁡h=I↾T⁡h∧h∈T∧h≠I↾B→U∘s=I↾T
27 14 20 22 24 25 26 syl131anc ⊢K∈HL∧W∈H∧h∈T∧h≠I↾B∧s∈E∧s≠0˙→U∘s=I↾T