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 = Base K
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 ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ s ⁡ h ∧ R ⁡ b ≠ R ⁡ g → z ⁡ Q = Y
cdleml6.u ⊢ U = g ∈ T ⟼ if s ⁡ h = h g X
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 = Base K
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 ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ s ⁡ h ∧ R ⁡ b ≠ R ⁡ g → z ⁡ Q = Y
11 cdleml6.u ⊢ U = g ∈ T ⟼ if s ⁡ h = h g X
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