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	|- .<_ = ( le ` K )
	dia2dimlem10.j	|- .\/ = ( join ` K )
	dia2dimlem10.a	|- A = ( Atoms ` K )
	dia2dimlem10.h	|- H = ( LHyp ` K )
	dia2dimlem10.t	|- T = ( ( LTrn ` K ) ` W )
	dia2dimlem10.r	|- R = ( ( trL ` K ) ` W )
	dia2dimlem10.y	|- Y = ( ( DVecA ` K ) ` W )
	dia2dimlem10.s	|- S = ( LSubSp ` Y )
	dia2dimlem10.n	|- N = ( LSpan ` Y )
	dia2dimlem10.i	|- I = ( ( DIsoA ` K ) ` W )
	dia2dimlem10.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dia2dimlem10.u	|- ( ph -> ( U e. A /\ U .<_ W ) )
	dia2dimlem10.v	|- ( ph -> ( V e. A /\ V .<_ W ) )
	dia2dimlem10.f	|- ( ph -> F e. T )
	dia2dimlem10.fe	|- ( ph -> F e. ( I ` ( U .\/ V ) ) )
Assertion	dia2dimlem10	|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )

Proof

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