Theorem djhjlj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 9-Aug-2014)

	Ref	Expression
Hypotheses	djhj.k	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	djhj.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	djhj.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	djhj.j	$$⊢J=\mathrm{joinH}\left(K\right)\left(W\right)$$
	djhj.w	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	djhj.x	$$⊢\phi \to X\in \mathrm{ran}I$$
	djhj.y	$$⊢\phi \to Y\in \mathrm{ran}I$$
Assertion	djhjlj	$$⊢\phi \to XJY=I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		djhj.k	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
2		djhj.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		djhj.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		djhj.j	$$⊢J=\mathrm{joinH}\left(K\right)\left(W\right)$$
5		djhj.w	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		djhj.x	$$⊢\phi \to X\in \mathrm{ran}I$$
7		djhj.y	$$⊢\phi \to Y\in \mathrm{ran}I$$
8		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
9	8 2 3	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$$
10	5 6 9	syl2anc	$$⊢\phi \to I^{-1}\left(X\right)\in {\mathrm{Base}}_K$$
11	8 2 3	dihcnvcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Y\in \mathrm{ran}I\right)\to I^{-1}\left(Y\right)\in {\mathrm{Base}}_K$$
12	5 7 11	syl2anc	$$⊢\phi \to I^{-1}\left(Y\right)\in {\mathrm{Base}}_K$$
13	8 1 2 3 4	djhlj	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(I^{-1}\left(X\right)\in {\mathrm{Base}}_K\wedge I^{-1}\left(Y\right)\in {\mathrm{Base}}_K\right)\right)\to I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)=I\left(I^{-1}\left(X\right)\right)JI\left(I^{-1}\left(Y\right)\right)$$
14	5 10 12 13	syl12anc	$$⊢\phi \to I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)=I\left(I^{-1}\left(X\right)\right)JI\left(I^{-1}\left(Y\right)\right)$$
15	2 3	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$$
16	5 6 15	syl2anc	$$⊢\phi \to I\left(I^{-1}\left(X\right)\right)=X$$
17	2 3	dihcnvid2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Y\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(Y\right)\right)=Y$$
18	5 7 17	syl2anc	$$⊢\phi \to I\left(I^{-1}\left(Y\right)\right)=Y$$
19	16 18	oveq12d	$$⊢\phi \to I\left(I^{-1}\left(X\right)\right)JI\left(I^{-1}\left(Y\right)\right)=XJY$$
20	14 19	eqtr2d	$$⊢\phi \to XJY=I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)$$