Theorem llnexatN

Description: Given an atom on a line, there is another atom whose join equals the line. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	llnexat.l	⊢ ≤ = ( le ‘ 𝐾 )
	llnexat.j	⊢ ∨ = ( join ‘ 𝐾 )
	llnexat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	llnexat.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion	llnexatN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) )

Proof

Step	Hyp	Ref	Expression
1		llnexat.l	⊢ ≤ = ( le ‘ 𝐾 )
2		llnexat.j	⊢ ∨ = ( join ‘ 𝐾 )
3		llnexat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		llnexat.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
5		simp1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ HL )
6		simp3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
7		simp2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → 𝑋 ∈ 𝑁 )
8	5 6 7	3jca	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) )
9		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
10	1 9 3 4	atcvrlln2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ( ⋖ ‘ 𝐾 ) 𝑋 )
11	8 10	sylan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ( ⋖ ‘ 𝐾 ) 𝑋 )
12		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝐾 ∈ HL )
13		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ∈ 𝐴 )
14		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15	14 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
16	13 15	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
17		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ∈ 𝑁 )
18	14 4	llnbase	⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
19	17 18	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
20	14 1 2 9 3	cvrval3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ) )
21	12 16 19 20	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ) )
22		simpll1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → 𝐾 ∈ HL )
23		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
24	22 23	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
25		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
26		simpll3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
27	1 3	atncmp	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑞 ≤ 𝑃 ↔ 𝑞 ≠ 𝑃 ) )
28	24 25 26 27	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ≤ 𝑃 ↔ 𝑞 ≠ 𝑃 ) )
29	28	anbi1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( ¬ 𝑞 ≤ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ↔ ( 𝑞 ≠ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ) )
30		necom	⊢ ( 𝑞 ≠ 𝑃 ↔ 𝑃 ≠ 𝑞 )
31		eqcom	⊢ ( ( 𝑃 ∨ 𝑞 ) = 𝑋 ↔ 𝑋 = ( 𝑃 ∨ 𝑞 ) )
32	30 31	anbi12i	⊢ ( ( 𝑞 ≠ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ↔ ( 𝑃 ≠ 𝑞 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) )
33	29 32	bitrdi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( ¬ 𝑞 ≤ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ↔ ( 𝑃 ≠ 𝑞 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) ) )
34	33	rexbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑃 ∧ ( 𝑃 ∨ 𝑞 ) = 𝑋 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) ) )
35	21 34	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) ) )
36	11 35	mpbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) )