Metamath Proof Explorer

Theorem cdlemc3

Description: Part of proof of Lemma C in Crawley p. 113. (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses cdlemc3.l ⊢ ≤ ˙ = ≤ K
cdlemc3.j ⊢ ∨ ˙ = join ⁡ K
cdlemc3.m ⊢ ∧ ˙ = meet ⁡ K
cdlemc3.a ⊢ A = Atoms ⁡ K
cdlemc3.h ⊢ H = LHyp ⁡ K
cdlemc3.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemc3.r ⊢ R = trL ⁡ K ⁡ W
Assertion cdlemc3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F → Q ≤ ˙ P ∨ ˙ F ⁡ P

Proof

Step Hyp Ref Expression
1 cdlemc3.l ⊢ ≤ ˙ = ≤ K
2 cdlemc3.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemc3.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemc3.a ⊢ A = Atoms ⁡ K
5 cdlemc3.h ⊢ H = LHyp ⁡ K
6 cdlemc3.t ⊢ T = LTrn ⁡ K ⁡ W
7 cdlemc3.r ⊢ R = trL ⁡ K ⁡ W
8 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ HL
9 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ HL ∧ W ∈ H
10 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ∈ T
11 simpr2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∈ A
12 1 4 5 6 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A → F ⁡ P ∈ A
13 9 10 11 12 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ∈ A
14 simpr3l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∈ A
15 eqid ⊢ Base K = Base K
16 15 5 6 7 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ∈ Base K
17 10 16 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → R ⁡ F ∈ Base K
18 1 4 5 6 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W
19 18 3adant3r3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W
20 1 4 5 6 7 trlnle ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W → ¬ F ⁡ P ≤ ˙ R ⁡ F
21 9 10 19 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → ¬ F ⁡ P ≤ ˙ R ⁡ F
22 15 1 2 4 hlexch2 ⊢ K ∈ HL ∧ F ⁡ P ∈ A ∧ Q ∈ A ∧ R ⁡ F ∈ Base K ∧ ¬ F ⁡ P ≤ ˙ R ⁡ F → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F → Q ≤ ˙ F ⁡ P ∨ ˙ R ⁡ F
23 8 13 14 17 21 22 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F → Q ≤ ˙ F ⁡ P ∨ ˙ R ⁡ F
24 1 2 4 5 6 7 trljat2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ P ∨ ˙ R ⁡ F = P ∨ ˙ F ⁡ P
25 24 3adant3r3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ∨ ˙ R ⁡ F = P ∨ ˙ F ⁡ P
26 25 breq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ≤ ˙ F ⁡ P ∨ ˙ R ⁡ F ↔ Q ≤ ˙ P ∨ ˙ F ⁡ P
27 23 26 sylibd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F → Q ≤ ˙ P ∨ ˙ F ⁡ P