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 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑦 ∨ 𝑧 ) ∧ 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) )