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_ℋ )

Metamath Proof Explorer

Theorem chscl

Proof