Theorem islpln2

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012)

	Ref	Expression
Hypotheses	islpln5.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	islpln5.l	⊢ ≤ = ( le ‘ 𝐾 )
	islpln5.j	⊢ ∨ = ( join ‘ 𝐾 )
	islpln5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	islpln5.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	islpln2	⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islpln5.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		islpln5.l	⊢ ≤ = ( le ‘ 𝐾 )
3		islpln5.j	⊢ ∨ = ( join ‘ 𝐾 )
4		islpln5.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		islpln5.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6	1 5	lplnbase	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ 𝐵 )
7	6	pm4.71ri	⊢ ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) )
8	1 2 3 4 5	islpln5	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
9	8	pm5.32da	⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
10	7 9	syl5bb	⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )