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	$$⊢\phi \to A\in {\mathbf{C}}_{\mathscr{H}}$$
	chscl.2	$$⊢\phi \to B\in {\mathbf{C}}_{\mathscr{H}}$$
	chscl.3	$$⊢\phi \to B\subseteq \perp \left(A\right)$$
Assertion	chscl	$$⊢\phi \to A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		chscl.1	$$⊢\phi \to A\in {\mathbf{C}}_{\mathscr{H}}$$
2		chscl.2	$$⊢\phi \to B\in {\mathbf{C}}_{\mathscr{H}}$$
3		chscl.3	$$⊢\phi \to B\subseteq \perp \left(A\right)$$
4		chsh	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\in {\mathbf{S}}_{\mathscr{H}}$$
5	1 4	syl	$$⊢\phi \to A\in {\mathbf{S}}_{\mathscr{H}}$$
6		chsh	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to B\in {\mathbf{S}}_{\mathscr{H}}$$
7	2 6	syl	$$⊢\phi \to B\in {\mathbf{S}}_{\mathscr{H}}$$
8		shscl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}$$
9	5 7 8	syl2anc	$$⊢\phi \to A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}$$
10	1	adantr	$$⊢\left(\phi \wedge \left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\right)\to A\in {\mathbf{C}}_{\mathscr{H}}$$
11	2	adantr	$$⊢\left(\phi \wedge \left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\right)\to B\in {\mathbf{C}}_{\mathscr{H}}$$
12	3	adantr	$$⊢\left(\phi \wedge \left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\right)\to B\subseteq \perp \left(A\right)$$
13		simprl	$$⊢\left(\phi \wedge \left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\right)\to f:\mathbb{N}⟶A{+}_{\mathscr{H}}B$$
14		simprr	$$⊢\left(\phi \wedge \left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\right)\to f\underset{v}{⇝}z$$
15		eqid	$$⊢\left(x\in \mathbb{N}⟼{\mathrm{proj}}_{ℎ}\left(A\right)\left(f\left(x\right)\right)\right)=\left(x\in \mathbb{N}⟼{\mathrm{proj}}_{ℎ}\left(A\right)\left(f\left(x\right)\right)\right)$$
16		eqid	$$⊢\left(x\in \mathbb{N}⟼{\mathrm{proj}}_{ℎ}\left(B\right)\left(f\left(x\right)\right)\right)=\left(x\in \mathbb{N}⟼{\mathrm{proj}}_{ℎ}\left(B\right)\left(f\left(x\right)\right)\right)$$
17	10 11 12 13 14 15 16	chscllem4	$$⊢\left(\phi \wedge \left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\right)\to z\in \left(A{+}_{\mathscr{H}}B\right)$$
18	17	ex	$$⊢\phi \to \left(\left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\to z\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
19	18	alrimivv	$$⊢\phi \to \forall f\forall z\left(\left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\to z\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
20		isch2	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow \left(A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}\wedge \forall f\forall z\left(\left(f:\mathbb{N}⟶A{+}_{\mathscr{H}}B\wedge f\underset{v}{⇝}z\right)\to z\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)$$
21	9 19 20	sylanbrc	$$⊢\phi \to A{+}_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$