Theorem cdlemg5

Description: TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? TODO: The .\/ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg5.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemg5.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemg5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemg5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	cdlemg5	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemg5.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg5.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemg5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		cdlemg5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5	1 3 4	lhpexle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑊 )
6	5	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑊 )
7		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) ) → ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) )
9		simplr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
10	1 2 3 4	cdlemf1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ) )
11	7 8 9 10	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ) )
12		3simpa	⊢ ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ) → ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ) )
13	12	reximi	⊢ ( ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ) )
14	11 13	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑟 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ) )
15	6 14	rexlimddv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ) )