This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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