Metamath Proof Explorer

Theorem dia2dimlem12

Description: Lemma for dia2dim . Obtain subset relation. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem12.l 
|- .<_ = ( le ` K )
dia2dimlem12.j 
|- .\/ = ( join ` K )
dia2dimlem12.m 
|- ./\ = ( meet ` K )
dia2dimlem12.a 
|- A = ( Atoms ` K )
dia2dimlem12.h 
|- H = ( LHyp ` K )
dia2dimlem12.t 
|- T = ( ( LTrn ` K ) ` W )
dia2dimlem12.r 
|- R = ( ( trL ` K ) ` W )
dia2dimlem12.y 
|- Y = ( ( DVecA ` K ) ` W )
dia2dimlem12.s 
|- S = ( LSubSp ` Y )
dia2dimlem12.pl 
|- .(+) = ( LSSum ` Y )
dia2dimlem12.n 
|- N = ( LSpan ` Y )
dia2dimlem12.i 
|- I = ( ( DIsoA ` K ) ` W )
dia2dimlem12.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dia2dimlem12.u 
|- ( ph -> ( U e. A /\ U .<_ W ) )
dia2dimlem12.v 
|- ( ph -> ( V e. A /\ V .<_ W ) )
dia2dimlem12.uv 
|- ( ph -> U =/= V )
Assertion dia2dimlem12 
|- ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )

Proof

Step Hyp Ref Expression
1 dia2dimlem12.l 
 |-  .<_ = ( le ` K )
2 dia2dimlem12.j 
 |-  .\/ = ( join ` K )
3 dia2dimlem12.m 
 |-  ./\ = ( meet ` K )
4 dia2dimlem12.a 
 |-  A = ( Atoms ` K )
5 dia2dimlem12.h 
 |-  H = ( LHyp ` K )
6 dia2dimlem12.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 dia2dimlem12.r 
 |-  R = ( ( trL ` K ) ` W )
8 dia2dimlem12.y 
 |-  Y = ( ( DVecA ` K ) ` W )
9 dia2dimlem12.s 
 |-  S = ( LSubSp ` Y )
10 dia2dimlem12.pl 
 |-  .(+) = ( LSSum ` Y )
11 dia2dimlem12.n 
 |-  N = ( LSpan ` Y )
12 dia2dimlem12.i 
 |-  I = ( ( DIsoA ` K ) ` W )
13 dia2dimlem12.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
14 dia2dimlem12.u 
 |-  ( ph -> ( U e. A /\ U .<_ W ) )
15 dia2dimlem12.v 
 |-  ( ph -> ( V e. A /\ V .<_ W ) )
16 dia2dimlem12.uv 
 |-  ( ph -> U =/= V )
17 13 simpld 
 |-  ( ph -> K e. HL )
18 14 simpld 
 |-  ( ph -> U e. A )
19 15 simpld 
 |-  ( ph -> V e. A )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 20 2 4 hlatjcl 
 |-  ( ( K e. HL /\ U e. A /\ V e. A ) -> ( U .\/ V ) e. ( Base ` K ) )
22 17 18 19 21 syl3anc 
 |-  ( ph -> ( U .\/ V ) e. ( Base ` K ) )
23 14 simprd 
 |-  ( ph -> U .<_ W )
24 15 simprd 
 |-  ( ph -> V .<_ W )
25 17 hllatd 
 |-  ( ph -> K e. Lat )
26 20 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
27 18 26 syl 
 |-  ( ph -> U e. ( Base ` K ) )
28 20 4 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
29 19 28 syl 
 |-  ( ph -> V e. ( Base ` K ) )
30 13 simprd 
 |-  ( ph -> W e. H )
31 20 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
32 30 31 syl 
 |-  ( ph -> W e. ( Base ` K ) )
33 20 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 ) )
34 25 27 29 32 33 syl13anc 
 |-  ( ph -> ( ( U .<_ W /\ V .<_ W ) <-> ( U .\/ V ) .<_ W ) )
35 23 24 34 mpbi2and 
 |-  ( ph -> ( U .\/ V ) .<_ W )
36 20 1 5 6 12 diass 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( U .\/ V ) e. ( Base ` K ) /\ ( U .\/ V ) .<_ W ) ) -> ( I ` ( U .\/ V ) ) C_ T )
37 13 22 35 36 syl12anc 
 |-  ( ph -> ( I ` ( U .\/ V ) ) C_ T )
38 37 sseld 
 |-  ( ph -> ( f e. ( I ` ( U .\/ V ) ) -> f e. T ) )
39 13 3ad2ant1 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> ( K e. HL /\ W e. H ) )
40 14 3ad2ant1 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> ( U e. A /\ U .<_ W ) )
41 15 3ad2ant1 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> ( V e. A /\ V .<_ W ) )
42 simp3 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> f e. T )
43 16 3ad2ant1 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> U =/= V )
44 simp2 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> f e. ( I ` ( U .\/ V ) ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 39 40 41 42 43 44 dia2dimlem11 
 |-  ( ( ph /\ f e. ( I ` ( U .\/ V ) ) /\ f e. T ) -> f e. ( ( I ` U ) .(+) ( I ` V ) ) )
46 45 3exp 
 |-  ( ph -> ( f e. ( I ` ( U .\/ V ) ) -> ( f e. T -> f e. ( ( I ` U ) .(+) ( I ` V ) ) ) ) )
47 38 46 mpdd 
 |-  ( ph -> ( f e. ( I ` ( U .\/ V ) ) -> f e. ( ( I ` U ) .(+) ( I ` V ) ) ) )
48 47 ssrdv 
 |-  ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )