Theorem dia2dimlem10

Description: Lemma for dia2dim . Convert membership in closed subspace ( I( U .\/ V ) ) to a lattice ordering. (Contributed by NM, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem10.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dimlem10.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dimlem10.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		dia2dimlem10.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		dia2dimlem10.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		dia2dimlem10.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
7		dia2dimlem10.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
8		dia2dimlem10.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
9		dia2dimlem10.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
10		dia2dimlem10.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
11		dia2dimlem10.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		dia2dimlem10.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
13		dia2dimlem10.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
14		dia2dimlem10.f	$$⊢\phi \to F\in T$$
15		dia2dimlem10.fe	$$⊢\phi \to F\in I\left(U\underset{\dot{}}{\vee }V\right)$$
16	4 5 6 7 10 9	dia1dim2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to I\left(R\left(F\right)\right)=N\left(\left\{F\right\}\right)$$
17	11 14 16	syl2anc	$$⊢\phi \to I\left(R\left(F\right)\right)=N\left(\left\{F\right\}\right)$$
18	4 7	dvalvec	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to Y\in \mathrm{LVec}$$
19		lveclmod	$$⊢Y\in \mathrm{LVec}\to Y\in \mathrm{LMod}$$
20	11 18 19	3syl	$$⊢\phi \to Y\in \mathrm{LMod}$$
21	11	simpld	$$⊢\phi \to K\in \mathrm{HL}$$
22	12	simpld	$$⊢\phi \to U\in A$$
23	13	simpld	$$⊢\phi \to V\in A$$
24		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
25	24 2 3	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$$
26	21 22 23 25	syl3anc	$$⊢\phi \to U\underset{\dot{}}{\vee }V\in {\mathrm{Base}}_K$$
27	12	simprd	$$⊢\phi \to U\underset{\dot{}}{\le }W$$
28	13	simprd	$$⊢\phi \to V\underset{\dot{}}{\le }W$$
29	21	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$
30	24 3	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
31	22 30	syl	$$⊢\phi \to U\in {\mathrm{Base}}_K$$
32	24 3	atbase	$$⊢V\in A\to V\in {\mathrm{Base}}_K$$
33	23 32	syl	$$⊢\phi \to V\in {\mathrm{Base}}_K$$
34	11	simprd	$$⊢\phi \to W\in H$$
35	24 4	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
36	34 35	syl	$$⊢\phi \to W\in {\mathrm{Base}}_K$$
37	24 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)$$
38	29 31 33 36 37	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)$$
39	27 28 38	mpbi2and	$$⊢\phi \to \left(U\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }W$$
40	24 1 4 7 10 8	dialss	$$⊢\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)\in S$$
41	11 26 39 40	syl12anc	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\in S$$
42	8 9 20 41 15	ellspsn5	$$⊢\phi \to N\left(\left\{F\right\}\right)\subseteq I\left(U\underset{\dot{}}{\vee }V\right)$$
43	17 42	eqsstrd	$$⊢\phi \to I\left(R\left(F\right)\right)\subseteq I\left(U\underset{\dot{}}{\vee }V\right)$$
44	24 4 5 6	trlcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to R\left(F\right)\in {\mathrm{Base}}_K$$
45	11 14 44	syl2anc	$$⊢\phi \to R\left(F\right)\in {\mathrm{Base}}_K$$
46	1 4 5 6	trlle	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to R\left(F\right)\underset{\dot{}}{\le }W$$
47	11 14 46	syl2anc	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }W$$
48	24 1 4 10	diaord	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(R\left(F\right)\in {\mathrm{Base}}_K\wedge R\left(F\right)\underset{\dot{}}{\le }W\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 \left(I\left(R\left(F\right)\right)\subseteq I\left(U\underset{\dot{}}{\vee }V\right)\leftrightarrow R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)\right)$$
49	11 45 47 26 39 48	syl122anc	$$⊢\phi \to \left(I\left(R\left(F\right)\right)\subseteq I\left(U\underset{\dot{}}{\vee }V\right)\leftrightarrow R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)\right)$$
50	43 49	mpbid	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)$$