Metamath Proof Explorer

Theorem dia2dimlem13

Description: Lemma for dia2dim . Eliminate U =/= V condition. (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 ) )
Assertion dia2dimlem13 
|- ( 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 oveq2 
 |-  ( U = V -> ( U .\/ U ) = ( U .\/ V ) )
17 16 adantl 
 |-  ( ( ph /\ U = V ) -> ( U .\/ U ) = ( U .\/ V ) )
18 13 simpld 
 |-  ( ph -> K e. HL )
19 14 simpld 
 |-  ( ph -> U e. A )
20 2 4 hlatjidm 
 |-  ( ( K e. HL /\ U e. A ) -> ( U .\/ U ) = U )
21 18 19 20 syl2anc 
 |-  ( ph -> ( U .\/ U ) = U )
22 21 adantr 
 |-  ( ( ph /\ U = V ) -> ( U .\/ U ) = U )
23 17 22 eqtr3d 
 |-  ( ( ph /\ U = V ) -> ( U .\/ V ) = U )
24 23 fveq2d 
 |-  ( ( ph /\ U = V ) -> ( I ` ( U .\/ V ) ) = ( I ` U ) )
25 ssid 
 |-  ( I ` U ) C_ ( I ` U )
26 24 25 eqsstrdi 
 |-  ( ( ph /\ U = V ) -> ( I ` ( U .\/ V ) ) C_ ( I ` U ) )
27 5 8 dvalvec 
 |-  ( ( K e. HL /\ W e. H ) -> Y e. LVec )
28 lveclmod 
 |-  ( Y e. LVec -> Y e. LMod )
29 13 27 28 3syl 
 |-  ( ph -> Y e. LMod )
30 eqid 
 |-  ( Base ` K ) = ( Base ` K )
31 30 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
32 19 31 syl 
 |-  ( ph -> U e. ( Base ` K ) )
33 14 simprd 
 |-  ( ph -> U .<_ W )
34 30 1 5 8 12 9 dialss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. ( Base ` K ) /\ U .<_ W ) ) -> ( I ` U ) e. S )
35 13 32 33 34 syl12anc 
 |-  ( ph -> ( I ` U ) e. S )
36 9 lsssubg 
 |-  ( ( Y e. LMod /\ ( I ` U ) e. S ) -> ( I ` U ) e. ( SubGrp ` Y ) )
37 29 35 36 syl2anc 
 |-  ( ph -> ( I ` U ) e. ( SubGrp ` Y ) )
38 10 lsmidm 
 |-  ( ( I ` U ) e. ( SubGrp ` Y ) -> ( ( I ` U ) .(+) ( I ` U ) ) = ( I ` U ) )
39 37 38 syl 
 |-  ( ph -> ( ( I ` U ) .(+) ( I ` U ) ) = ( I ` U ) )
40 fveq2 
 |-  ( U = V -> ( I ` U ) = ( I ` V ) )
41 40 oveq2d 
 |-  ( U = V -> ( ( I ` U ) .(+) ( I ` U ) ) = ( ( I ` U ) .(+) ( I ` V ) ) )
42 39 41 sylan9req 
 |-  ( ( ph /\ U = V ) -> ( I ` U ) = ( ( I ` U ) .(+) ( I ` V ) ) )
43 26 42 sseqtrd 
 |-  ( ( ph /\ U = V ) -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
44 13 adantr 
 |-  ( ( ph /\ U =/= V ) -> ( K e. HL /\ W e. H ) )
45 14 adantr 
 |-  ( ( ph /\ U =/= V ) -> ( U e. A /\ U .<_ W ) )
46 15 adantr 
 |-  ( ( ph /\ U =/= V ) -> ( V e. A /\ V .<_ W ) )
47 simpr 
 |-  ( ( ph /\ U =/= V ) -> U =/= V )
48 1 2 3 4 5 6 7 8 9 10 11 12 44 45 46 47 dia2dimlem12 
 |-  ( ( ph /\ U =/= V ) -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
49 43 48 pm2.61dane 
 |-  ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )