Theorem chcv1

Description: The Hilbert lattice has the covering property. Proposition 1(ii) of Kalmbach p. 140 (and its converse). (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chcv1	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		atom1d	⊢ ( 𝐵 ∈ HAtoms ↔ ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) )
2		spansncv2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( ¬ ( span ‘ { 𝑥 } ) ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) )
3		sseq1	⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐵 ⊆ 𝐴 ↔ ( span ‘ { 𝑥 } ) ⊆ 𝐴 ) )
4	3	notbid	⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ ¬ ( span ‘ { 𝑥 } ) ⊆ 𝐴 ) )
5		oveq2	⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) )
6	5	breq2d	⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) )
7	4 6	imbi12d	⊢ ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ¬ ( span ‘ { 𝑥 } ) ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝑥 } ) ) ) ) )
8	2 7	syl5ibrcom	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐵 = ( span ‘ { 𝑥 } ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
9	8	adantld	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
10	9	rexlimdva	⊢ ( 𝐴 ∈ Cℋ → ( ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
11	10	imp	⊢ ( ( 𝐴 ∈ Cℋ ∧ ∃ 𝑥 ∈ ℋ ( 𝑥 ≠ 0ℎ ∧ 𝐵 = ( span ‘ { 𝑥 } ) ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
12	1 11	sylan2b	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
13		atelch	⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
14		chjcl	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
15		cvpss	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) )
16	14 15	syldan	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) )
17		chnle	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) )
18	16 17	sylibrd	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → ¬ 𝐵 ⊆ 𝐴 ) )
19	13 18	sylan2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → ¬ 𝐵 ⊆ 𝐴 ) )
20	12 19	impbid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )