Theorem dia2dimlem12

Description: Lemma for dia2dim . Obtain subset relation. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dia2dimlem12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dia2dimlem12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dia2dimlem12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dia2dimlem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dia2dimlem12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dia2dimlem12.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dia2dimlem12.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dia2dimlem12.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
	dia2dimlem12.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
	dia2dimlem12.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
	dia2dimlem12.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	dia2dimlem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dia2dimlem12.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
	dia2dimlem12.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
	dia2dimlem12.uv	$$⊢\phi \to U\ne V$$
Assertion	dia2dimlem12	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dimlem12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dimlem12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dia2dimlem12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dia2dimlem12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		dia2dimlem12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		dia2dimlem12.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		dia2dimlem12.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
9		dia2dimlem12.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
10		dia2dimlem12.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
11		dia2dimlem12.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
12		dia2dimlem12.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
13		dia2dimlem12.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		dia2dimlem12.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
15		dia2dimlem12.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
16		dia2dimlem12.uv	$$⊢\phi \to U\ne V$$
17	13	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
18	14	simpld	$$⊢\phi \to U\in A$$
19	15	simpld	$$⊢\phi \to V\in A$$
20		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
21	20 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge U\in A\wedge V\in A\right)\to U\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
22	17 18 19 21	syl3anc	$$⊢\phi \to U\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
23	14	simprd	$$⊢\phi \to U\underset{\dot{}}{\le }W$$
24	15	simprd	$$⊢\phi \to V\underset{\dot{}}{\le }W$$
25	17	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
26	20 4	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
27	18 26	syl	$$⊢\phi \to U\in {\mathrm{Base}}_K$$
28	20 4	atbase	$$⊢V\in A\to V\in {\mathrm{Base}}_K$$
29	19 28	syl	$$⊢\phi \to V\in {\mathrm{Base}}_K$$
30	13	simprd	$$⊢\phi \to W\in H$$
31	20 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
32	30 31	syl	$$⊢\phi \to W\in {\mathrm{Base}}_K$$
33	20 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(U\in {\mathrm{Base}}_K\wedge V\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(U\underset{\dot{}}{\le }W\wedge V\underset{\dot{}}{\le }W\right)\leftrightarrow \left(U\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }W\right)$$
34	25 27 29 32 33	syl13anc	$$⊢\phi \to \left(\left(U\underset{\dot{}}{\le }W\wedge V\underset{\dot{}}{\le }W\right)\leftrightarrow \left(U\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }W\right)$$
35	23 24 34	mpbi2and	$$⊢\phi \to \left(U\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }W$$
36	20 1 5 6 12	diass	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(U\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K\wedge \left(U\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }W\right)\right)\to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq T$$
37	13 22 35 36	syl12anc	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq T$$
38	37	sseld	$$⊢\phi \to \left(f\in I\left(U\underset{\dot{}}{\vee }V\right)\to f\in T\right)$$
39	13	3ad2ant1	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
40	14	3ad2ant1	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
41	15	3ad2ant1	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
42		simp3	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to f\in T$$
43	16	3ad2ant1	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to U\ne V$$
44		simp2	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to f\in I\left(U\underset{\dot{}}{\vee }V\right)$$
45	1 2 3 4 5 6 7 8 9 10 11 12 39 40 41 42 43 44	dia2dimlem11	$$⊢\left(\phi \wedge f\in I\left(U\underset{\dot{}}{\vee }V\right)\wedge f\in T\right)\to f\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$
46	45	3exp	$$⊢\phi \to \left(f\in I\left(U\underset{\dot{}}{\vee }V\right)\to \left(f\in T\to f\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)\right)\right)$$
47	38 46	mpdd	$$⊢\phi \to \left(f\in I\left(U\underset{\dot{}}{\vee }V\right)\to f\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)\right)$$
48	47	ssrdv	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$