Theorem lplni

Description: Condition implying a lattice plane. (Contributed by NM, 20-Jun-2012)

	Ref	Expression
Hypotheses	lplnset.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lplnset.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	lplnset.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
	lplnset.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	lplni	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		lplnset.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lplnset.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		lplnset.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
4		lplnset.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5		simpl2	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝐵 )
6		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐶 𝑌 ↔ 𝑋 𝐶 𝑌 ) )
7	6	rspcev	⊢ ( ( 𝑋 ∈ 𝑁 ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑥 ∈ 𝑁 𝑥 𝐶 𝑌 )
8	7	3ad2antl3	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑥 ∈ 𝑁 𝑥 𝐶 𝑌 )
9		simpl1	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑋 𝐶 𝑌 ) → 𝐾 ∈ 𝐷 )
10	1 2 3 4	islpln	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑁 𝑥 𝐶 𝑌 ) ) )
11	9 10	syl	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑁 𝑥 𝐶 𝑌 ) ) )
12	5 8 11	mpbir2and	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝑃 )