Metamath Proof Explorer

Theorem chscl

Description: The subspace sum of two closed orthogonal spaces is closed. (Contributed by NM, 19-Oct-1999) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses chscl.1 ⊢ ( 𝜑 → 𝐴 ∈ Cℋ )
chscl.2 ⊢ ( 𝜑 → 𝐵 ∈ Cℋ )
chscl.3 ⊢ ( 𝜑 → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
Assertion chscl ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ )

Proof

Step Hyp Ref Expression
1 chscl.1 ⊢ ( 𝜑 → 𝐴 ∈ Cℋ )
2 chscl.2 ⊢ ( 𝜑 → 𝐵 ∈ Cℋ )
3 chscl.3 ⊢ ( 𝜑 → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
4 chsh ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
5 1 4 syl ⊢ ( 𝜑 → 𝐴 ∈ Sℋ )
6 chsh ⊢ ( 𝐵 ∈ Cℋ → 𝐵 ∈ Sℋ )
7 2 6 syl ⊢ ( 𝜑 → 𝐵 ∈ Sℋ )
8 shscl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ )
9 5 7 8 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) ) → 𝐴 ∈ Cℋ )
11 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) ) → 𝐵 ∈ Cℋ )
12 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) ) → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) ) → 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) ) → 𝑓 ⇝𝑣 𝑧 )
15 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
16 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ( ( projℎ ‘ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ( ( projℎ ‘ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
17 10 11 12 13 14 15 16 chscllem4 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) ) → 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) )
18 17 ex ⊢ ( 𝜑 → ( ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) → 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
19 18 alrimivv ⊢ ( 𝜑 → ∀ 𝑓 ∀ 𝑧 ( ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) → 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
20 isch2 ⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ ↔ ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑧 ( ( 𝑓 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑓 ⇝𝑣 𝑧 ) → 𝑧 ∈ ( 𝐴 +ℋ 𝐵 ) ) ) )
21 9 19 20 sylanbrc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ )