Theorem djhj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-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	djhj	$$⊢\phi \to I^{-1}\left(XJY\right)=I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\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	1 2 3 4 5 6 7	djhjlj	$$⊢\phi \to XJY=I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)$$
9	8	fveq2d	$$⊢\phi \to I^{-1}\left(XJY\right)=I^{-1}\left(I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)\right)$$
10	5	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
11	10	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
12		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
13	12 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$$
14	5 6 13	syl2anc	$$⊢\phi \to I^{-1}\left(X\right)\in {\mathrm{Base}}_K$$
15	12 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$$
16	5 7 15	syl2anc	$$⊢\phi \to I^{-1}\left(Y\right)\in {\mathrm{Base}}_K$$
17	12 1	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge I^{-1}\left(X\right)\in {\mathrm{Base}}_K\wedge I^{-1}\left(Y\right)\in {\mathrm{Base}}_K\right)\to I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\in {\mathrm{Base}}_K$$
18	11 14 16 17	syl3anc	$$⊢\phi \to I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\in {\mathrm{Base}}_K$$
19	12 2 3	dihcnvid1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\in {\mathrm{Base}}_K\right)\to I^{-1}\left(I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)\right)=I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)$$
20	5 18 19	syl2anc	$$⊢\phi \to I^{-1}\left(I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)\right)\right)=I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)$$
21	9 20	eqtrd	$$⊢\phi \to I^{-1}\left(XJY\right)=I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Y\right)$$