This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemkyuu

Description: cdlemkyu with some hypotheses eliminated. TODO: Clean all this up. (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
cdlemk5c.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
cdlemk5a.u2 ⊢ C = e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ S ⁡ b ⁡ P ∨ ˙ R ⁡ e ∘ b -1
Assertion cdlemkyuu ⊢ 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 → ⦋ G / g⦌ Y = C ⁡ G ⁡ P

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 cdlemk5c.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
12 cdlemk5a.u2 ⊢ C = e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ S ⁡ b ⁡ P ∨ ˙ R ⁡ e ∘ b -1
13 eqid ⊢ d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ S ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 = d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ S ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1
14 eqid ⊢ S ⁡ b = S ⁡ b
15 1 2 3 4 5 6 7 8 9 10 11 13 14 12 cdlemkyu ⊢ 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 → ⦋ G / g⦌ Y = C ⁡ G ⁡ P