Metamath Proof Explorer

Theorem dia2dimlem9

Description: Lemma for dia2dim . Eliminate ( RF ) =/= U , V conditions. (Contributed by NM, 8-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dia2dimlem9.l 
 |-  .<_ = ( le ` K )
2 dia2dimlem9.j 
 |-  .\/ = ( join ` K )
3 dia2dimlem9.m 
 |-  ./\ = ( meet ` K )
4 dia2dimlem9.a 
 |-  A = ( Atoms ` K )
5 dia2dimlem9.h 
 |-  H = ( LHyp ` K )
6 dia2dimlem9.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 dia2dimlem9.r 
 |-  R = ( ( trL ` K ) ` W )
8 dia2dimlem9.y 
 |-  Y = ( ( DVecA ` K ) ` W )
9 dia2dimlem9.s 
 |-  S = ( LSubSp ` Y )
10 dia2dimlem9.pl 
 |-  .(+) = ( LSSum ` Y )
11 dia2dimlem9.n 
 |-  N = ( LSpan ` Y )
12 dia2dimlem9.i 
 |-  I = ( ( DIsoA ` K ) ` W )
13 dia2dimlem9.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
14 dia2dimlem9.u 
 |-  ( ph -> ( U e. A /\ U .<_ W ) )
15 dia2dimlem9.v 
 |-  ( ph -> ( V e. A /\ V .<_ W ) )
16 dia2dimlem9.f 
 |-  ( ph -> F e. T )
17 dia2dimlem9.rf 
 |-  ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
18 dia2dimlem9.uv 
 |-  ( ph -> U =/= V )
19 5 8 dvalvec 
 |-  ( ( K e. HL /\ W e. H ) -> Y e. LVec )
20 lveclmod 
 |-  ( Y e. LVec -> Y e. LMod )
21 9 lsssssubg 
 |-  ( Y e. LMod -> S C_ ( SubGrp ` Y ) )
22 13 19 20 21 4syl 
 |-  ( ph -> S C_ ( SubGrp ` Y ) )
23 14 simpld 
 |-  ( ph -> U e. A )
24 eqid 
 |-  ( Base ` K ) = ( Base ` K )
25 24 4 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
26 23 25 syl 
 |-  ( ph -> U e. ( Base ` K ) )
27 14 simprd 
 |-  ( ph -> U .<_ W )
28 24 1 5 8 12 9 dialss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. ( Base ` K ) /\ U .<_ W ) ) -> ( I ` U ) e. S )
29 13 26 27 28 syl12anc 
 |-  ( ph -> ( I ` U ) e. S )
30 22 29 sseldd 
 |-  ( ph -> ( I ` U ) e. ( SubGrp ` Y ) )
31 15 simpld 
 |-  ( ph -> V e. A )
32 24 4 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
33 31 32 syl 
 |-  ( ph -> V e. ( Base ` K ) )
34 15 simprd 
 |-  ( ph -> V .<_ W )
35 24 1 5 8 12 9 dialss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( V e. ( Base ` K ) /\ V .<_ W ) ) -> ( I ` V ) e. S )
36 13 33 34 35 syl12anc 
 |-  ( ph -> ( I ` V ) e. S )
37 22 36 sseldd 
 |-  ( ph -> ( I ` V ) e. ( SubGrp ` Y ) )
38 10 lsmub1 
 |-  ( ( ( I ` U ) e. ( SubGrp ` Y ) /\ ( I ` V ) e. ( SubGrp ` Y ) ) -> ( I ` U ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
39 30 37 38 syl2anc 
 |-  ( ph -> ( I ` U ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
40 39 adantr 
 |-  ( ( ph /\ ( R ` F ) = U ) -> ( I ` U ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
41 5 6 7 12 dia1dimid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( I ` ( R ` F ) ) )
42 13 16 41 syl2anc 
 |-  ( ph -> F e. ( I ` ( R ` F ) ) )
43 42 adantr 
 |-  ( ( ph /\ ( R ` F ) = U ) -> F e. ( I ` ( R ` F ) ) )
44 fveq2 
 |-  ( ( R ` F ) = U -> ( I ` ( R ` F ) ) = ( I ` U ) )
45 44 adantl 
 |-  ( ( ph /\ ( R ` F ) = U ) -> ( I ` ( R ` F ) ) = ( I ` U ) )
46 43 45 eleqtrd 
 |-  ( ( ph /\ ( R ` F ) = U ) -> F e. ( I ` U ) )
47 40 46 sseldd 
 |-  ( ( ph /\ ( R ` F ) = U ) -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
48 30 adantr 
 |-  ( ( ph /\ ( R ` F ) = V ) -> ( I ` U ) e. ( SubGrp ` Y ) )
49 37 adantr 
 |-  ( ( ph /\ ( R ` F ) = V ) -> ( I ` V ) e. ( SubGrp ` Y ) )
50 10 lsmub2 
 |-  ( ( ( I ` U ) e. ( SubGrp ` Y ) /\ ( I ` V ) e. ( SubGrp ` Y ) ) -> ( I ` V ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
51 48 49 50 syl2anc 
 |-  ( ( ph /\ ( R ` F ) = V ) -> ( I ` V ) C_ ( ( I ` U ) .(+) ( I ` V ) ) )
52 42 adantr 
 |-  ( ( ph /\ ( R ` F ) = V ) -> F e. ( I ` ( R ` F ) ) )
53 fveq2 
 |-  ( ( R ` F ) = V -> ( I ` ( R ` F ) ) = ( I ` V ) )
54 53 adantl 
 |-  ( ( ph /\ ( R ` F ) = V ) -> ( I ` ( R ` F ) ) = ( I ` V ) )
55 52 54 eleqtrd 
 |-  ( ( ph /\ ( R ` F ) = V ) -> F e. ( I ` V ) )
56 51 55 sseldd 
 |-  ( ( ph /\ ( R ` F ) = V ) -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
57 13 adantr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> ( K e. HL /\ W e. H ) )
58 14 adantr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> ( U e. A /\ U .<_ W ) )
59 15 adantr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> ( V e. A /\ V .<_ W ) )
60 16 adantr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> F e. T )
61 17 adantr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> ( R ` F ) .<_ ( U .\/ V ) )
62 18 adantr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> U =/= V )
63 simprl 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> ( R ` F ) =/= U )
64 simprr 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> ( R ` F ) =/= V )
65 1 2 3 4 5 6 7 8 9 10 11 12 57 58 59 60 61 62 63 64 dia2dimlem8 
 |-  ( ( ph /\ ( ( R ` F ) =/= U /\ ( R ` F ) =/= V ) ) -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )
66 47 56 65 pm2.61da2ne 
 |-  ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )