Theorem dihjat4

Description: Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015)

	Ref	Expression
Hypotheses	dihjat4.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihjat4.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihjat4.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihjat4.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihjat4.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihjat4.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dihjat4.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihjat4.x	$$⊢\phi \to X\in \mathrm{ran}I$$
	dihjat4.q	$$⊢\phi \to Q\in A$$
Assertion	dihjat4	$$⊢\phi \to X\underset{\dot{}}{\oplus }Q=I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Q\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihjat4.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
2		dihjat4.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihjat4.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		dihjat4.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dihjat4.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
6		dihjat4.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
7		dihjat4.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		dihjat4.x	$$⊢\phi \to X\in \mathrm{ran}I$$
9		dihjat4.q	$$⊢\phi \to Q\in A$$
10		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
11		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
12	10 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$$
13	7 8 12	syl2anc	$$⊢\phi \to I^{-1}\left(X\right)\in {\mathrm{Base}}_K$$
14	11 2 4 3 6	dihlatat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Q\in A\right)\to I^{-1}\left(Q\right)\in \mathrm{Atoms}\left(K\right)$$
15	7 9 14	syl2anc	$$⊢\phi \to I^{-1}\left(Q\right)\in \mathrm{Atoms}\left(K\right)$$
16	10 2 1 11 4 5 3 7 13 15	dihjat3	$$⊢\phi \to I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Q\right)\right)=I\left(I^{-1}\left(X\right)\right)\underset{\dot{}}{\oplus }I\left(I^{-1}\left(Q\right)\right)$$
17	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$$
18	7 8 17	syl2anc	$$⊢\phi \to I\left(I^{-1}\left(X\right)\right)=X$$
19	2 4 3 6	dih1dimat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Q\in A\right)\to Q\in \mathrm{ran}I$$
20	7 9 19	syl2anc	$$⊢\phi \to Q\in \mathrm{ran}I$$
21	2 3	dihcnvid2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Q\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(Q\right)\right)=Q$$
22	7 20 21	syl2anc	$$⊢\phi \to I\left(I^{-1}\left(Q\right)\right)=Q$$
23	18 22	oveq12d	$$⊢\phi \to I\left(I^{-1}\left(X\right)\right)\underset{\dot{}}{\oplus }I\left(I^{-1}\left(Q\right)\right)=X\underset{\dot{}}{\oplus }Q$$
24	16 23	eqtr2d	$$⊢\phi \to X\underset{\dot{}}{\oplus }Q=I\left(I^{-1}\left(X\right)\underset{\dot{}}{\vee }{I}^{-1}\left(Q\right)\right)$$