Theorem lhpjat1

Description: The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	lhpjat.l	⊢ ≤ = ( le ‘ 𝐾 )
	lhpjat.j	⊢ ∨ = ( join ‘ 𝐾 )
	lhpjat.u	⊢ 1 = ( 1. ‘ 𝐾 )
	lhpjat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lhpjat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhpjat1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑃 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		lhpjat.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhpjat.j	⊢ ∨ = ( join ‘ 𝐾 )
3		lhpjat.u	⊢ 1 = ( 1. ‘ 𝐾 )
4		lhpjat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		lhpjat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
9	8	ad2antlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
10		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
11		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
12	3 11 5	lhp1cvr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) 1 )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑊 ( ⋖ ‘ 𝐾 ) 1 )
14		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ¬ 𝑃 ≤ 𝑊 )
15	7 1 2 3 11 4	1cvrjat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑊 ( ⋖ ‘ 𝐾 ) 1 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑃 ) = 1 )
16	6 9 10 13 14 15	syl32anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑊 ∨ 𝑃 ) = 1 )