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

Metamath Proof Explorer

Theorem cdlemk13

Description: Part of proof of Lemma K of Crawley p. 118. Line 13 on p. 119. O , D are k_1, f_1. (Contributed by NM, 1-Jul-2013)

Ref Expression
Hypotheses cdlemk1.b ⊢ B = Base K
cdlemk1.l ⊢ ≤ ˙ = ≤ K
cdlemk1.j ⊢ ∨ ˙ = join ⁡ K
cdlemk1.m ⊢ ∧ ˙ = meet ⁡ K
cdlemk1.a ⊢ A = Atoms ⁡ K
cdlemk1.h ⊢ H = LHyp ⁡ K
cdlemk1.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemk1.r ⊢ R = trL ⁡ K ⁡ W
cdlemk1.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
cdlemk1.o ⊢ O = S ⁡ D
Assertion cdlemk13 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ D ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ D ≠ I ↾ B ∧ R ⁡ D ≠ R ⁡ F → O ⁡ P = P ∨ ˙ R ⁡ D ∧ ˙ N ⁡ P ∨ ˙ R ⁡ D ∘ F -1

Proof

Step Hyp Ref Expression
1 cdlemk1.b ⊢ B = Base K
2 cdlemk1.l ⊢ ≤ ˙ = ≤ K
3 cdlemk1.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk1.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemk1.a ⊢ A = Atoms ⁡ K
6 cdlemk1.h ⊢ H = LHyp ⁡ K
7 cdlemk1.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemk1.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemk1.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
10 cdlemk1.o ⊢ O = S ⁡ D
11 10 fveq1i ⊢ O ⁡ P = S ⁡ D ⁡ P
12 1 2 3 5 6 7 8 4 9 cdlemksv2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ D ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ D ≠ I ↾ B ∧ R ⁡ D ≠ R ⁡ F → S ⁡ D ⁡ P = P ∨ ˙ R ⁡ D ∧ ˙ N ⁡ P ∨ ˙ R ⁡ D ∘ F -1
13 11 12 eqtrid ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ D ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ D ≠ I ↾ B ∧ R ⁡ D ≠ R ⁡ F → O ⁡ P = P ∨ ˙ R ⁡ D ∧ ˙ N ⁡ P ∨ ˙ R ⁡ D ∘ F -1