This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ { 𝐵 } ) ) ) )