Metamath Proof Explorer


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 ) )