Theorem dih2dimb

Description: Extend dib2dim to isomorphism H. (Contributed by NM, 22-Sep-2014)

	Ref	Expression
Hypotheses	dih2dimb.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dih2dimb.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dih2dimb.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dih2dimb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dih2dimb.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dih2dimb.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dih2dimb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dih2dimb.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dih2dimb.p	$$⊢\phi \to \left(P\in A\wedge P\underset{\dot{}}{\le }W\right)$$
	dih2dimb.q	$$⊢\phi \to \left(Q\in A\wedge Q\underset{\dot{}}{\le }W\right)$$
Assertion	dih2dimb	$$⊢\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		dih2dimb.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dih2dimb.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dih2dimb.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		dih2dimb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		dih2dimb.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		dih2dimb.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
7		dih2dimb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
8		dih2dimb.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dih2dimb.p	$$⊢\phi \to \left(P\in A\wedge P\underset{\dot{}}{\le }W\right)$$
10		dih2dimb.q	$$⊢\phi \to \left(Q\in A\wedge Q\underset{\dot{}}{\le }W\right)$$
11		eqid	$$⊢\mathrm{DIsoB}\left(K\right)\left(W\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
12	1 2 3 4 5 6 11 8 9 10	dib2dim	$$⊢\phi \to \mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)\subseteq \mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\right)\underset{\dot{}}{\oplus }\mathrm{DIsoB}\left(K\right)\left(W\right)\left(Q\right)$$
13	8	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
14	9	simpld	$$⊢\phi \to P\in A$$
15	10	simpld	$$⊢\phi \to Q\in A$$
16		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
17	16 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$$
18	13 14 15 17	syl3anc	$$⊢\phi \to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
19	9	simprd	$$⊢\phi \to P\underset{\dot{}}{\le }W$$
20	10	simprd	$$⊢\phi \to Q\underset{\dot{}}{\le }W$$
21	13	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
22	16 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
23	14 22	syl	$$⊢\phi \to P\in {\mathrm{Base}}_K$$
24	16 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
25	15 24	syl	$$⊢\phi \to Q\in {\mathrm{Base}}_K$$
26	8	simprd	$$⊢\phi \to W\in H$$
27	16 4	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
28	26 27	syl	$$⊢\phi \to W\in {\mathrm{Base}}_K$$
29	16 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)$$
30	21 23 25 28 29	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)$$
31	19 20 30	mpbi2and	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }W$$
32	16 1 4 7 11	dihvalb	$$⊢\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 I\left(P\underset{\dot{}}{\vee }Q\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)$$
33	8 18 31 32	syl12anc	$$⊢\phi \to I\left(P\underset{\dot{}}{\vee }Q\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\underset{\dot{}}{\vee }Q\right)$$
34	16 1 4 7 11	dihvalb	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\le }W\right)\right)\to I\left(P\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\right)$$
35	8 23 19 34	syl12anc	$$⊢\phi \to I\left(P\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\right)$$
36	16 1 4 7 11	dihvalb	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(Q\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(Q\right)$$
37	8 25 20 36	syl12anc	$$⊢\phi \to I\left(Q\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(Q\right)$$
38	35 37	oveq12d	$$⊢\phi \to I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)\left(P\right)\underset{\dot{}}{\oplus }\mathrm{DIsoB}\left(K\right)\left(W\right)\left(Q\right)$$
39	12 33 38	3sstr4d	$$⊢\phi \to I\left(P\underset{\dot{}}{\vee }Q\right)\subseteq I\left(P\right)\underset{\dot{}}{\oplus }I\left(Q\right)$$