Metamath Proof Explorer

Theorem cdlemc4

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

Ref Expression
Hypotheses cdlemc3.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemc3.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemc3.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemc3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemc3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemc3.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemc3.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemc4 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ≠ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemc3.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemc3.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemc3.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdlemc3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemc3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemc3.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 cdlemc3.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
10 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐹 ∈ 𝑇 )
12 simpr2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑃 ∈ 𝐴 )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
15 12 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
16 13 5 6 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
17 10 11 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
18 simpr3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑄 ∈ 𝐴 )
19 13 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
20 8 12 18 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
21 13 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 21 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
23 13 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
24 9 20 22 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
25 13 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
26 9 17 24 25 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
27 breq2 ⊢ ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ↔ ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
28 26 27 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ) )
29 1 2 3 4 5 6 7 cdlemc3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) )
30 28 29 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) )
31 30 necon3bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) → ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ≠ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
32 31 3impia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ≠ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )