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