Metamath Proof Explorer

Theorem cdleme11fN

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme11.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme11.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme11.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme11.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme11.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme11.c ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
cdleme11.d ⊢ 𝐷 = ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 )
cdleme11.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
Assertion cdleme11fN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐹 ≠ 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme11.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme11.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme11.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme11.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme11.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme11.c ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
8 cdleme11.d ⊢ 𝐷 = ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 )
9 cdleme11.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
10 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
11 10 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ Lat )
12 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
15 12 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
16 simp23l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ 𝐴 )
17 13 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
18 16 17 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
19 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
20 11 15 18 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
21 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
22 13 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
23 21 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
24 13 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
25 11 20 23 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
26 7 25 eqbrtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐶 ≤ 𝑊 )
27 1 2 3 4 5 6 9 cdleme3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝐹 ≤ 𝑊 )
28 nbrne2 ⊢ ( ( 𝐶 ≤ 𝑊 ∧ ¬ 𝐹 ≤ 𝑊 ) → 𝐶 ≠ 𝐹 )
29 28 necomd ⊢ ( ( 𝐶 ≤ 𝑊 ∧ ¬ 𝐹 ≤ 𝑊 ) → 𝐹 ≠ 𝐶 )
30 26 27 29 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐹 ≠ 𝐶 )