Metamath Proof Explorer

Theorem cdleme21h

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)

Ref Expression
Hypotheses cdleme21.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme21.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme21.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme21.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme21.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme21.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme21.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
cdleme21g.g ⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
cdleme21g.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
cdleme21g.y ⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
cdleme21g.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
cdleme21g.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) )
Assertion cdleme21h ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) → ( ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) → 𝑁 = 𝑂 ) )

Proof

Step Hyp Ref Expression
1 cdleme21.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme21.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme21.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme21.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme21.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme21.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme21.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8 cdleme21g.g ⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
9 cdleme21g.d ⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
10 cdleme21g.y ⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
11 cdleme21g.n ⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
12 cdleme21g.o ⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) )
13 simp11 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
14 simp12 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
15 simp13l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
16 simp13r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) )
17 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → 𝑧 ∈ 𝐴 )
18 simp3l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑧 ≤ 𝑊 )
19 simp3r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) )
20 17 18 19 jca31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 cdleme21g ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑁 = 𝑂 )
22 13 14 15 16 20 21 syl113anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → 𝑁 = 𝑂 )
23 22 rexlimdv3a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) → ( ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) → 𝑁 = 𝑂 ) )