Theorem pjjsi

Description: A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjjs.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjjs.2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	pjjsi	$$⊢\forall x\in \left(G{\vee }_{\mathscr{H}}H\right){\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\to G{\vee }_{\mathscr{H}}H=G{+}_{\mathscr{H}}H$$

Proof

Step	Hyp	Ref	Expression
1		pjjs.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjjs.2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
3		fveq2	$$⊢x=w\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)$$
4	3	eleq1d	$$⊢x=w\to \left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)$$
5	4	rspcv	$$⊢w\in \left(G{\vee }_{\mathscr{H}}H\right)\to \left(\forall x\in \left(G{\vee }_{\mathscr{H}}H\right){\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)$$
6	1	chshii	$$⊢G\in {\mathbf{S}}_{\mathscr{H}}$$
7	6 2	shjcli	$$⊢G{\vee }_{\mathscr{H}}H\in {\mathbf{C}}_{\mathscr{H}}$$
8	7	cheli	$$⊢w\in \left(G{\vee }_{\mathscr{H}}H\right)\to w\in \mathscr{H}$$
9	1	pjcli	$$⊢w\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right)\in G$$
10	9	anim1i	$$⊢\left(w\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right)\in G\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)$$
11		axpjpj	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge w\in \mathscr{H}\right)\to w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)$$
12	1 11	mpan	$$⊢w\in \mathscr{H}\to w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)$$
13	12	adantr	$$⊢\left(w\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\to w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)$$
14	10 13	jca	$$⊢\left(w\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right)\in G\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\wedge w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\right)$$
15	8 14	sylan	$$⊢\left(w\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right)\in G\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\wedge w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\right)$$
16		rspceov	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right)\in G\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\wedge w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\right)\to \exists y\in G\exists z\in Hw=y{+}_{ℎ}z$$
17	16	3expa	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right)\in G\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\wedge w={\mathrm{proj}}_{ℎ}\left(G\right)\left(w\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\right)\to \exists y\in G\exists z\in Hw=y{+}_{ℎ}z$$
18	15 17	syl	$$⊢\left(w\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\to \exists y\in G\exists z\in Hw=y{+}_{ℎ}z$$
19	6 2	shseli	$$⊢w\in \left(G{+}_{\mathscr{H}}H\right)\leftrightarrow \exists y\in G\exists z\in Hw=y{+}_{ℎ}z$$
20	18 19	sylibr	$$⊢\left(w\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\right)\to w\in \left(G{+}_{\mathscr{H}}H\right)$$
21	20	ex	$$⊢w\in \left(G{\vee }_{\mathscr{H}}H\right)\to \left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(w\right)\in H\to w\in \left(G{+}_{\mathscr{H}}H\right)\right)$$
22	5 21	syldc	$$⊢\forall x\in \left(G{\vee }_{\mathscr{H}}H\right){\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\to \left(w\in \left(G{\vee }_{\mathscr{H}}H\right)\to w\in \left(G{+}_{\mathscr{H}}H\right)\right)$$
23	22	ssrdv	$$⊢\forall x\in \left(G{\vee }_{\mathscr{H}}H\right){\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\to G{\vee }_{\mathscr{H}}H\subseteq G{+}_{\mathscr{H}}H$$
24	6 2	shsleji	$$⊢G{+}_{\mathscr{H}}H\subseteq G{\vee }_{\mathscr{H}}H$$
25	23 24	jctir	$$⊢\forall x\in \left(G{\vee }_{\mathscr{H}}H\right){\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\to \left(G{\vee }_{\mathscr{H}}H\subseteq G{+}_{\mathscr{H}}H\wedge G{+}_{\mathscr{H}}H\subseteq G{\vee }_{\mathscr{H}}H\right)$$
26		eqss	$$⊢G{\vee }_{\mathscr{H}}H=G{+}_{\mathscr{H}}H\leftrightarrow \left(G{\vee }_{\mathscr{H}}H\subseteq G{+}_{\mathscr{H}}H\wedge G{+}_{\mathscr{H}}H\subseteq G{\vee }_{\mathscr{H}}H\right)$$
27	25 26	sylibr	$$⊢\forall x\in \left(G{\vee }_{\mathscr{H}}H\right){\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(x\right)\in H\to G{\vee }_{\mathscr{H}}H=G{+}_{\mathscr{H}}H$$