Theorem dihjat5N

Description: Transfer lattice join with atom to subspace sum. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihjat5.b	$$⊢B={\mathrm{Base}}_K$$
	dihjat5.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihjat5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihjat5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihjat5.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihjat5.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihjat5.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihjat5.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihjat5.x	$$⊢\phi \to X\in B$$
	dihjat5.p	$$⊢\phi \to P\in A$$
Assertion	dihjat5N	$$⊢\phi \to X\underset{\dot{}}{\vee }P=I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihjat5.b	$$⊢B={\mathrm{Base}}_K$$
2		dihjat5.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihjat5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihjat5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dihjat5.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		dihjat5.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
7		dihjat5.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
8		dihjat5.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dihjat5.x	$$⊢\phi \to X\in B$$
10		dihjat5.p	$$⊢\phi \to P\in A$$
11	1 2 3 4 5 6 7 8 9 10	dihjat3	$$⊢\phi \to I\left(X\underset{\dot{}}{\vee }P\right)=I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$
12		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
13	1 2 7	dihcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\right)\in \mathrm{ran}I$$
14	8 9 13	syl2anc	$$⊢\phi \to I\left(X\right)\in \mathrm{ran}I$$
15	4 2 5 7 12	dihatlat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge P\in A\right)\to I\left(P\right)\in \mathrm{LSAtoms}\left(U\right)$$
16	8 10 15	syl2anc	$$⊢\phi \to I\left(P\right)\in \mathrm{LSAtoms}\left(U\right)$$
17	2 7 5 6 12 8 14 16	dihsmatrn	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\in \mathrm{ran}I$$
18	2 7	dihcnvid2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)=I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$
19	8 17 18	syl2anc	$$⊢\phi \to I\left(I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)=I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)$$
20	11 19	eqtr4d	$$⊢\phi \to I\left(X\underset{\dot{}}{\vee }P\right)=I\left(I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)$$
21	8	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
22	21	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
23	1 4	atbase	$$⊢P\in A\to P\in B$$
24	10 23	syl	$$⊢\phi \to P\in B$$
25	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge P\in B\right)\to X\underset{\dot{}}{\vee }P\in B$$
26	22 9 24 25	syl3anc	$$⊢\phi \to X\underset{\dot{}}{\vee }P\in B$$
27	1 2 7	dihcnvcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\in \mathrm{ran}I\right)\to I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\in B$$
28	8 17 27	syl2anc	$$⊢\phi \to I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\in B$$
29	1 2 7	dih11	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\underset{\dot{}}{\vee }P\in B\wedge I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\in B\right)\to \left(I\left(X\underset{\dot{}}{\vee }P\right)=I\left(I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }P=I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)$$
30	8 26 28 29	syl3anc	$$⊢\phi \to \left(I\left(X\underset{\dot{}}{\vee }P\right)=I\left(I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }P=I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)\right)$$
31	20 30	mpbid	$$⊢\phi \to X\underset{\dot{}}{\vee }P=I^{-1}\left(I\left(X\right)\underset{\dot{}}{\oplus }I\left(P\right)\right)$$