Metamath Proof Explorer

Theorem cdlemk19y

Description: cdlemk19 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-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 cdlemk19y ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ b ∈ T ∧ b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F → ⦋ F / g⦌ Y = N ⁡ 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 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 cdlemk19ylem ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ b ∈ T ∧ b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F → ⦋ F / g⦌ Y = N ⁡ P