cdlemb3

Description: Given two atoms not under the fiducial co-atom W , there is a third. Lemma B in Crawley p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? Then replace cdlemb2 with it. This is a more general version of cdlemb2 without P =/= Q condition. (Contributed by NM, 27-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg5.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg5.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemg5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		cdlemg5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
7	1 2 3 4	cdlemg5	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑃 ≠ 𝑟 ∧ ¬ 𝑟 ≤ 𝑊 ) )
8	5 6 7	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑃 ≠ 𝑟 ∧ ¬ 𝑟 ≤ 𝑊 ) )
9		ancom	⊢ ( ( 𝑃 ≠ 𝑟 ∧ ¬ 𝑟 ≤ 𝑊 ) ↔ ( ¬ 𝑟 ≤ 𝑊 ∧ 𝑃 ≠ 𝑟 ) )
10		eqcom	⊢ ( 𝑃 = 𝑟 ↔ 𝑟 = 𝑃 )
11		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → 𝑃 = 𝑄 )
12	11	oveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = ( 𝑃 ∨ 𝑄 ) )
13		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ HL )
14		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
15	2 3	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = 𝑃 )
16	13 14 15	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑃 ) = 𝑃 )
17	12 16	eqtr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) = 𝑃 )
18	17	breq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑟 ≤ 𝑃 ) )
19		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
20	13 19	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
21		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐴 )
22	1 3	atcmp	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑟 ≤ 𝑃 ↔ 𝑟 = 𝑃 ) )
23	20 21 14 22	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ≤ 𝑃 ↔ 𝑟 = 𝑃 ) )
24	18 23	bitr2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 = 𝑃 ↔ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
25	10 24	syl5bb	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 = 𝑟 ↔ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
26	25	necon3abid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑟 ↔ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
27	26	anbi2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( ( ¬ 𝑟 ≤ 𝑊 ∧ 𝑃 ≠ 𝑟 ) ↔ ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
28	9 27	syl5bb	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑟 ∧ ¬ 𝑟 ≤ 𝑊 ) ↔ ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
29	28	3expa	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑟 ∧ ¬ 𝑟 ≤ 𝑊 ) ↔ ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
30	29	rexbidva	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 ≠ 𝑟 ∧ ¬ 𝑟 ≤ 𝑊 ) ↔ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
31	8 30	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 = 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
32		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
34		simpl3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
35		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
36	1 2 3 4	cdlemb2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
37	32 33 34 35 36	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )
38	31 37	pm2.61dane	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )

Metamath Proof Explorer

Theorem cdlemb3

Proof