Theorem djh01

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	djh01	$$⊢\phi \to X\underset{\dot{}}{\vee }\left\{\underset{\dot{}}{0}\right\}=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{join}\left(K\right)=\mathrm{join}\left(K\right)$$
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	6 9	syl	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{ran}I$$
11	8 1 4 5 6 7 10	djhjlj	$$⊢\phi \to X\underset{\dot{}}{\vee }\left\{\underset{\dot{}}{0}\right\}=I\left(I^{-1}\left(X\right)\mathrm{join}\left(K\right)I^{-1}\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)$$
12		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
13	1 12 4 2 3	dih0cnv	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I^{-1}\left(\left\{\underset{\dot{}}{0}\right\}\right)=\mathrm{0.}\left(K\right)$$
14	6 13	syl	$$⊢\phi \to I^{-1}\left(\left\{\underset{\dot{}}{0}\right\}\right)=\mathrm{0.}\left(K\right)$$
15	14	oveq2d	$$⊢\phi \to I^{-1}\left(X\right)\mathrm{join}\left(K\right)I^{-1}\left(\left\{\underset{\dot{}}{0}\right\}\right)=I^{-1}\left(X\right)\mathrm{join}\left(K\right)\mathrm{0.}\left(K\right)$$
16	6	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
17		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
18	16 17	syl	$$⊢\phi \to K\in \mathrm{OL}$$
19		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
20	19 1 4	dihcnvcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to I^{-1}\left(X\right)\in {\mathrm{Base}}_K$$
21	6 7 20	syl2anc	$$⊢\phi \to I^{-1}\left(X\right)\in {\mathrm{Base}}_K$$
22	19 8 12	olj01	$$⊢\left(K\in \mathrm{OL}\wedge I^{-1}\left(X\right)\in {\mathrm{Base}}_K\right)\to I^{-1}\left(X\right)\mathrm{join}\left(K\right)\mathrm{0.}\left(K\right)=I^{-1}\left(X\right)$$
23	18 21 22	syl2anc	$$⊢\phi \to I^{-1}\left(X\right)\mathrm{join}\left(K\right)\mathrm{0.}\left(K\right)=I^{-1}\left(X\right)$$
24	15 23	eqtrd	$$⊢\phi \to I^{-1}\left(X\right)\mathrm{join}\left(K\right)I^{-1}\left(\left\{\underset{\dot{}}{0}\right\}\right)=I^{-1}\left(X\right)$$
25	24	fveq2d	$$⊢\phi \to I\left(I^{-1}\left(X\right)\mathrm{join}\left(K\right)I^{-1}\left(\left\{\underset{\dot{}}{0}\right\}\right)\right)=I\left(I^{-1}\left(X\right)\right)$$
26	1 4	dihcnvid2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(X\right)\right)=X$$
27	6 7 26	syl2anc	$$⊢\phi \to I\left(I^{-1}\left(X\right)\right)=X$$
28	11 25 27	3eqtrd	$$⊢\phi \to X\underset{\dot{}}{\vee }\left\{\underset{\dot{}}{0}\right\}=X$$