Theorem djh02

Description: Closed subspace join with zero. (Contributed by NM, 9-Aug-2014)

	Ref	Expression
Hypotheses	djh01.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	djh01.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	djh01.o	$$⊢\underset{\dot{}}{0}=0_U$$
	djh01.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	djh01.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
	djh01.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	djh01.x	$$⊢\phi \to X\in \mathrm{ran}I$$
Assertion	djh02	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\vee }X=X$$

Proof

Step	Hyp	Ref	Expression
1		djh01.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		djh01.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		djh01.o	$$⊢\underset{\dot{}}{0}=0_U$$
4		djh01.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
5		djh01.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{joinH}\left(K\right)\left(W\right)$$
6		djh01.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		djh01.x	$$⊢\phi \to X\in \mathrm{ran}I$$
8		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
9	1 4 2 3	dih0rn	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{ran}I$$
10	1 2 4 8	dihrnss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{ran}I\right)\to \left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_U$$
11	6 9 10	syl2anc2	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_U$$
12	1 2 4 8	dihrnss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to X\subseteq {\mathrm{Base}}_U$$
13	6 7 12	syl2anc	$$⊢\phi \to X\subseteq {\mathrm{Base}}_U$$
14	1 2 8 5 6 11 13	djhcom	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }\left\{\underset{\dot{}}{0}\right\}$$
15	1 2 3 4 5 6 7	djh01	$$⊢\phi \to X\underset{\dot{}}{\vee }\left\{\underset{\dot{}}{0}\right\}=X$$
16	14 15	eqtrd	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\vee }X=X$$