Metamath Proof Explorer

Theorem cdlemk11tb

Description: Part of proof of Lemma K of Crawley p. 118. Lemma for Eq. 5, p. 119. G , I stand for g, h. cdlemk11ta with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b ⊢ B = Base K
cdlemk5.l ⊢ ≤ ˙ = ≤ K
cdlemk5.j ⊢ ∨ ˙ = join ⁡ K
cdlemk5.m ⊢ ∧ ˙ = meet ⁡ K
cdlemk5.a ⊢ A = Atoms ⁡ K
cdlemk5.h ⊢ H = LHyp ⁡ K
cdlemk5.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemk5.r ⊢ R = trL ⁡ K ⁡ W
cdlemk5.z ⊢ Z = P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1
cdlemk5.y ⊢ Y = P ∨ ˙ R ⁡ g ∧ ˙ Z ∨ ˙ R ⁡ g ∘ b -1
Assertion cdlemk11tb ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ G ∈ T ∧ G ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ b ∈ T ∧ b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G ∧ I ∈ T ∧ I ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ I → ⦋ G / g⦌ Y ≤ ˙ ⦋ I / g⦌ Y ∨ ˙ R ⁡ I ∘ G -1

Proof

Step Hyp Ref Expression
1 cdlemk5.b ⊢ B = Base K
2 cdlemk5.l ⊢ ≤ ˙ = ≤ K
3 cdlemk5.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk5.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemk5.a ⊢ A = Atoms ⁡ K
6 cdlemk5.h ⊢ H = LHyp ⁡ K
7 cdlemk5.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemk5.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemk5.z ⊢ Z = P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1
10 cdlemk5.y ⊢ Y = P ∨ ˙ R ⁡ g ∧ ˙ Z ∨ ˙ R ⁡ g ∘ b -1
11 eqid ⊢ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
12 eqid ⊢ e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ b ⁡ P ∨ ˙ R ⁡ e ∘ b -1 = e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ b ⁡ P ∨ ˙ R ⁡ e ∘ b -1
13 1 2 3 4 5 6 7 8 9 10 11 12 cdlemk11ta ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ G ∈ T ∧ G ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ b ∈ T ∧ b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G ∧ I ∈ T ∧ I ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ I → ⦋ G / g⦌ Y ≤ ˙ ⦋ I / g⦌ Y ∨ ˙ R ⁡ I ∘ G -1