This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem paddasslem7

Description: Lemma for paddass . Combine paddasslem5 and paddasslem6 . (Contributed by NM, 9-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddasslem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddasslem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddasslem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝐾 ∈ HL )
5 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ∈ 𝐴 )
6 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑠 ∈ 𝐴 )
7 5 6 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) )
8 simpl33 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑧 ∈ 𝐴 )
9 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑟 ∈ 𝐴 )
10 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
11 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) )
12 1 2 3 paddasslem5 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ) → 𝑠 ≠ 𝑧 )
13 4 9 10 11 12 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑠 ≠ 𝑧 )
14 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) )
15 1 2 3 paddasslem6 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) )
16 4 7 8 13 14 15 syl32anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) )