Metamath Proof Explorer

Theorem cdlemk35

Description: Part of proof of Lemma K of Crawley p. 118. cdlemk29-3 with shorter hypotheses. (Contributed by NM, 18-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 cdlemk4.b ⊢ B = Base K
2 cdlemk4.l ⊢ ≤ ˙ = ≤ K
3 cdlemk4.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk4.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemk4.a ⊢ A = Atoms ⁡ K
6 cdlemk4.h ⊢ H = LHyp ⁡ K
7 cdlemk4.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemk4.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemk4.z ⊢ Z = P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1
10 cdlemk4.y ⊢ Y = P ∨ ˙ R ⁡ G ∧ ˙ Z ∨ ˙ R ⁡ G ∘ b -1
11 cdlemk4.x ⊢ X = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = Y
12 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
13 eqid ⊢ d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 = d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1
14 eqid ⊢ ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z = b d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 G = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z = b d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 G
15 1 2 3 4 5 6 7 8 12 13 14 cdlemk34 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ G ∈ T ∧ G ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N → ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z = b d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 G = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
16 9 oveq1i ⊢ Z ∨ ˙ R ⁡ G ∘ b -1 = P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
17 16 oveq2i ⊢ P ∨ ˙ R ⁡ G ∧ ˙ Z ∨ ˙ R ⁡ G ∘ b -1 = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
18 10 17 eqtri ⊢ Y = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
19 18 eqeq2i ⊢ z ⁡ P = Y ↔ z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
20 19 imbi2i ⊢ b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = Y ↔ b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
21 20 ralbii ⊢ ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = Y ↔ ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
22 21 a1i ⊢ z ∈ T → ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = Y ↔ ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
23 22 riotabiia ⊢ ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = Y = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
24 11 23 eqtri ⊢ X = ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ P ∨ ˙ R ⁡ b ∧ ˙ N ⁡ P ∨ ˙ R ⁡ b ∘ F -1 ∨ ˙ R ⁡ G ∘ b -1
25 15 24 eqtr4di ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ G ∈ T ∧ G ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N → ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z = b d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 G = X
26 1 2 3 4 5 6 7 8 12 13 14 cdlemk29-3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ G ∈ T ∧ G ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N → ι z ∈ T | ∀ b ∈ T b ≠ I ↾ B ∧ R ⁡ b ≠ R ⁡ F ∧ R ⁡ b ≠ R ⁡ G → z = b d ∈ T , e ∈ T ⟼ ι j ∈ T | j ⁡ P = P ∨ ˙ R ⁡ e ∧ ˙ f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1 ⁡ d ⁡ P ∨ ˙ R ⁡ e ∘ d -1 G ∈ T
27 25 26 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ G ∈ T ∧ G ≠ I ↾ B ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N → X ∈ T