Theorem islpln3

Description: The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012)

	Ref	Expression
Hypotheses	islpln3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	islpln3.l	⊢ ≤ = ( le ‘ 𝐾 )
	islpln3.j	⊢ ∨ = ( join ‘ 𝐾 )
	islpln3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	islpln3.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
	islpln3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	islpln3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑦 ∈ 𝑁 ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islpln3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		islpln3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		islpln3.j	⊢ ∨ = ( join ‘ 𝐾 )
4		islpln3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		islpln3.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
6		islpln3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
7		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
8	1 7 5 6	islpln4	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑦 ∈ 𝑁 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
9		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) → 𝐾 ∈ HL )
10	1 5	llnbase	⊢ ( 𝑦 ∈ 𝑁 → 𝑦 ∈ 𝐵 )
11	10	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝐵 )
12		simplr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) → 𝑋 ∈ 𝐵 )
13	1 2 3 7 4	cvrval3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ) )
14	9 11 12 13	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ) )
15		eqcom	⊢ ( ( 𝑦 ∨ 𝑝 ) = 𝑋 ↔ 𝑋 = ( 𝑦 ∨ 𝑝 ) )
16	15	a1i	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑦 ∨ 𝑝 ) = 𝑋 ↔ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) )
17	16	anbi2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
18	17	rexbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
19	14 18	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑁 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
20	19	rexbidva	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑁 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑦 ∈ 𝑁 ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
21	8 20	bitrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑦 ∈ 𝑁 ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )