Theorem spansncv2

Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of Kalmbach p. 153. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansncv2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( ¬ ( span ‘ { 𝐵 } ) ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		spansncv	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) )
2	1	3exp	⊢ ( 𝐴 ∈ Cℋ → ( 𝑥 ∈ Cℋ → ( 𝐵 ∈ ℋ → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) ) )
3	2	com23	⊢ ( 𝐴 ∈ Cℋ → ( 𝐵 ∈ ℋ → ( 𝑥 ∈ Cℋ → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) ) )
4	3	imp	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ∈ Cℋ → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) )
5	4	ralrimiv	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) )
6	5	anim2i	⊢ ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∧ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∧ ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) )
7	6	expcom	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∧ ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) ) )
8		spansnch	⊢ ( 𝐵 ∈ ℋ → ( span ‘ { 𝐵 } ) ∈ Cℋ )
9		chnle	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( span ‘ { 𝐵 } ) ∈ Cℋ ) → ( ¬ ( span ‘ { 𝐵 } ) ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) )
10	8 9	sylan2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( ¬ ( span ‘ { 𝐵 } ) ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) )
11		chjcl	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( span ‘ { 𝐵 } ) ∈ Cℋ ) → ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∈ Cℋ )
12	8 11	sylan2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∈ Cℋ )
13		cvbr2	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∧ ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) ) )
14	12 13	syldan	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ∧ ∀ 𝑥 ∈ Cℋ ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) → 𝑥 = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) ) ) )
15	7 10 14	3imtr4d	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( ¬ ( span ‘ { 𝐵 } ) ⊆ 𝐴 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ) )