Theorem dib2dim

Description: Extend dia2dim to partial isomorphism B. (Contributed by NM, 22-Sep-2014)

	Ref	Expression
Hypotheses	dib2dim.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dib2dim.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dib2dim.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dib2dim.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dib2dim.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dib2dim.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dib2dim.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
	dib2dim.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dib2dim.p	$$⊢\phi \to \left(P\in A\wedge P\underset{\dot{}}{\le }W\right)$$
	dib2dim.q	$$⊢\phi \to \left(Q\in A\wedge Q\underset{\dot{}}{\le }W\right)$$
Assertion	dib2dim	$$⊢\phi \to I\left(P\underset{\dot{}}{\vee }Q\right)\subseteq I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		dib2dim.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dib2dim.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dib2dim.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		dib2dim.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		dib2dim.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		dib2dim.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
7		dib2dim.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
8		dib2dim.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dib2dim.p	$$⊢\phi \to \left(P\in A\wedge P\underset{\dot{}}{\le }W\right)$$
10		dib2dim.q	$$⊢\phi \to \left(Q\in A\wedge Q\underset{\dot{}}{\le }W\right)$$
11	4 7	dibvalrel	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{Rel}I\left(P\underset{\dot{}}{\vee }Q\right)$$
12	8 11	syl	$$⊢\phi \to \mathrm{Rel}I\left(P\underset{\dot{}}{\vee }Q\right)$$
13		eqid	$$⊢\mathrm{DVecA}\left(K\right)\left(W\right)=\mathrm{DVecA}\left(K\right)\left(W\right)$$
14		eqid	$$⊢\mathrm{LSSum}\left(\mathrm{DVecA}\left(K\right)\left(W\right)\right)=\mathrm{LSSum}\left(\mathrm{DVecA}\left(K\right)\left(W\right)\right)$$
15		eqid	$$⊢\mathrm{DIsoA}\left(K\right)\left(W\right)=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
16	1 2 3 4 13 14 15 8 9 10	dia2dim	$$⊢\phi \to \mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)\subseteq \mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\right)\mathrm{LSSum}\left(\mathrm{DVecA}\left(K\right)\left(W\right)\right)\mathrm{DIsoA}\left(K\right)\left(W\right)\left(Q\right)$$
17	16	sseld	$$⊢\phi \to \left(f\in \mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)\to f\in \left(\mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\right)\mathrm{LSSum}\left(\mathrm{DVecA}\left(K\right)\left(W\right)\right)\mathrm{DIsoA}\left(K\right)\left(W\right)\left(Q\right)\right)\right)$$
18	17	anim1d	$$⊢\phi \to \left(\left(f\in \mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)\wedge s=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)\right)\to \left(f\in \left(\mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\right)\mathrm{LSSum}\left(\mathrm{DVecA}\left(K\right)\left(W\right)\right)\mathrm{DIsoA}\left(K\right)\left(W\right)\left(Q\right)\right)\wedge s=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)\right)\right)$$
19	8	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
20	9	simpld	$$⊢\phi \to P\in A$$
21	10	simpld	$$⊢\phi \to Q\in A$$
22		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
23	22 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
24	19 20 21 23	syl3anc	$$⊢\phi \to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
25	9	simprd	$$⊢\phi \to P\underset{\dot{}}{\le }W$$
26	10	simprd	$$⊢\phi \to Q\underset{\dot{}}{\le }W$$
27	19	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
28	22 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
29	20 28	syl	$$⊢\phi \to P\in {\mathrm{Base}}_K$$
30	22 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
31	21 30	syl	$$⊢\phi \to Q\in {\mathrm{Base}}_K$$
32	8	simprd	$$⊢\phi \to W\in H$$
33	22 4	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
34	32 33	syl	$$⊢\phi \to W\in {\mathrm{Base}}_K$$
35	22 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(P\underset{\dot{}}{\le }W\wedge Q\underset{\dot{}}{\le }W\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }W\right)$$
36	27 29 31 34 35	syl13anc	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\le }W\wedge Q\underset{\dot{}}{\le }W\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }W\right)$$
37	25 26 36	mpbi2and	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }W$$
38		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
39		eqid	$$⊢\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)$$
40	22 1 4 38 39 15 7	dibopelval2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }W\right)\right)\to \left(⟨f,s⟩\in I\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \left(f\in \mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)\wedge s=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)\right)\right)$$
41	8 24 37 40	syl12anc	$$⊢\phi \to \left(⟨f,s⟩\in I\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \left(f\in \mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)\wedge s=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)\right)\right)$$
42	29 25	jca	$$⊢\phi \to \left(P\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\le }W\right)$$
43	31 26	jca	$$⊢\phi \to \left(Q\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\le }W\right)$$
44	22 1 4 38 39 13 5 14 6 15 7 8 42 43	diblsmopel	$$⊢\phi \to \left(⟨f,s⟩\in \left(I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)\right)\leftrightarrow \left(f\in \left(\mathrm{DIsoA}\left(K\right)\left(W\right)\left(P\right)\mathrm{LSSum}\left(\mathrm{DVecA}\left(K\right)\left(W\right)\right)\mathrm{DIsoA}\left(K\right)\left(W\right)\left(Q\right)\right)\wedge s=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K}\right)\right)\right)$$
45	18 41 44	3imtr4d	$$⊢\phi \to \left(⟨f,s⟩\in I\left(P\underset{\dot{}}{\vee }Q\right)\to ⟨f,s⟩\in \left(I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)\right)\right)$$
46	12 45	relssdv	$$⊢\phi \to I\left(P\underset{\dot{}}{\vee }Q\right)\subseteq I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)$$