Theorem 1dimN

Description: An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2dim.j	⊢ ∨ = ( join ‘ 𝐾 )
	2dim.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	2dim.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	1dimN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )

Proof

Step	Hyp	Ref	Expression
1		2dim.j	⊢ ∨ = ( join ‘ 𝐾 )
2		2dim.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		2dim.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4	1 2 3	2dim	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
5		r19.42v	⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
6	5	simplbi	⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )
7	6	reximi	⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → ∃ 𝑞 ∈ 𝐴 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )
8	4 7	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )