Metamath Proof Explorer

Theorem cdleme50ex

Description: Part of Lemma E in Crawley p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013)

Ref Expression
Hypotheses cdleme.l ⊢ ≤ ˙ = ≤ K
cdleme.a ⊢ A = Atoms ⁡ K
cdleme.h ⊢ H = LHyp ⁡ K
cdleme.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion cdleme50ex ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → ∃ f ∈ T f ⁡ P = Q

Proof

Step Hyp Ref Expression
1 cdleme.l ⊢ ≤ ˙ = ≤ K
2 cdleme.a ⊢ A = Atoms ⁡ K
3 cdleme.h ⊢ H = LHyp ⁡ K
4 cdleme.t ⊢ T = LTrn ⁡ K ⁡ W
5 eqid ⊢ Base K = Base K
6 eqid ⊢ join ⁡ K = join ⁡ K
7 eqid ⊢ meet ⁡ K = meet ⁡ K
8 eqid ⊢ P join ⁡ K Q meet ⁡ K W = P join ⁡ K Q meet ⁡ K W
9 eqid ⊢ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W = t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W
10 eqid ⊢ P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W
11 eqid ⊢ x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x = x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x
12 5 1 6 7 2 3 8 9 10 11 4 cdleme50ltrn ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ∈ T
13 5 1 6 7 2 3 8 9 10 11 cdleme17d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ P = Q
14 fveq1 ⊢ f = x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x → f ⁡ P = x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ P
15 14 eqeq1d ⊢ f = x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x → f ⁡ P = Q ↔ x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ P = Q
16 15 rspcev ⊢ x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ∈ T ∧ x ∈ Base K ⟼ if P ≠ Q ∧ ¬ x ≤ ˙ W ι z ∈ Base K | ∀ s ∈ A ¬ s ≤ ˙ W ∧ s join ⁡ K x meet ⁡ K W = x → z = if s ≤ ˙ P join ⁡ K Q ι y ∈ Base K | ∀ t ∈ A ¬ t ≤ ˙ W ∧ ¬ t ≤ ˙ P join ⁡ K Q → y = P join ⁡ K Q meet ⁡ K t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K s join ⁡ K t meet ⁡ K W ⦋ s / t⦌ t join ⁡ K P join ⁡ K Q meet ⁡ K W meet ⁡ K Q join ⁡ K P join ⁡ K t meet ⁡ K W join ⁡ K x meet ⁡ K W x ⁡ P = Q → ∃ f ∈ T f ⁡ P = Q
17 12 13 16 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → ∃ f ∈ T f ⁡ P = Q