Metamath Proof Explorer

Theorem paddasslem4

Description: Lemma for paddass . Combine paddasslem1 , paddasslem2 , and paddasslem3 . (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion paddasslem4 ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝐾 ∈ HL )
5 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑥 ∈ 𝐴 )
6 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑟 ∈ 𝐴 )
7 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑦 ∈ 𝐴 )
8 5 6 7 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
9 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ∈ 𝐴 )
10 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑧 ∈ 𝐴 )
11 9 10 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
12 4 8 11 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) )
13 simpl32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑥 ≠ 𝑦 )
14 simpl33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) )
15 1 2 3 paddasslem1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) → ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) )
16 4 8 13 14 15 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) )
17 simpl31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ≠ 𝑧 )
18 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) )
19 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
20 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) )
21 1 2 3 paddasslem2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) )
22 4 6 19 14 20 21 syl212anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) )
23 18 22 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) ) )
24 16 17 23 jca31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ( ( ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) ) ) )
25 1 2 3 paddasslem3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) )
26 12 24 25 sylc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) )