Metamath Proof Explorer

Theorem lcfrlem38

Description: Lemma for lcfr . Combine lcfrlem27 and lcfrlem37 . (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem38.h 
|- H = ( LHyp ` K )
lcfrlem38.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfrlem38.u 
|- U = ( ( DVecH ` K ) ` W )
lcfrlem38.p 
|- .+ = ( +g ` U )
lcfrlem38.f 
|- F = ( LFnl ` U )
lcfrlem38.l 
|- L = ( LKer ` U )
lcfrlem38.d 
|- D = ( LDual ` U )
lcfrlem38.q 
|- Q = ( LSubSp ` D )
lcfrlem38.c 
|- C = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcfrlem38.e 
|- E = U_ g e. G ( ._|_ ` ( L ` g ) )
lcfrlem38.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrlem38.g 
|- ( ph -> G e. Q )
lcfrlem38.gs 
|- ( ph -> G C_ C )
lcfrlem38.xe 
|- ( ph -> X e. E )
lcfrlem38.ye 
|- ( ph -> Y e. E )
lcfrlem38.z 
|- .0. = ( 0g ` U )
lcfrlem38.x 
|- ( ph -> X =/= .0. )
lcfrlem38.y 
|- ( ph -> Y =/= .0. )
lcfrlem38.sp 
|- N = ( LSpan ` U )
lcfrlem38.ne 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
lcfrlem38.b 
|- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
lcfrlem38.i 
|- ( ph -> I e. B )
lcfrlem38.n 
|- ( ph -> I =/= .0. )
lcfrlem38.v 
|- V = ( Base ` U )
lcfrlem38.t 
|- .x. = ( .s ` U )
lcfrlem38.s 
|- S = ( Scalar ` U )
lcfrlem38.r 
|- R = ( Base ` S )
lcfrlem38.j 
|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
Assertion lcfrlem38 
|- ( ph -> ( X .+ Y ) e. E )

Proof

Step Hyp Ref Expression
1 lcfrlem38.h 
 |-  H = ( LHyp ` K )
2 lcfrlem38.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfrlem38.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfrlem38.p 
 |-  .+ = ( +g ` U )
5 lcfrlem38.f 
 |-  F = ( LFnl ` U )
6 lcfrlem38.l 
 |-  L = ( LKer ` U )
7 lcfrlem38.d 
 |-  D = ( LDual ` U )
8 lcfrlem38.q 
 |-  Q = ( LSubSp ` D )
9 lcfrlem38.c 
 |-  C = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
10 lcfrlem38.e 
 |-  E = U_ g e. G ( ._|_ ` ( L ` g ) )
11 lcfrlem38.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 lcfrlem38.g 
 |-  ( ph -> G e. Q )
13 lcfrlem38.gs 
 |-  ( ph -> G C_ C )
14 lcfrlem38.xe 
 |-  ( ph -> X e. E )
15 lcfrlem38.ye 
 |-  ( ph -> Y e. E )
16 lcfrlem38.z 
 |-  .0. = ( 0g ` U )
17 lcfrlem38.x 
 |-  ( ph -> X =/= .0. )
18 lcfrlem38.y 
 |-  ( ph -> Y =/= .0. )
19 lcfrlem38.sp 
 |-  N = ( LSpan ` U )
20 lcfrlem38.ne 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
21 lcfrlem38.b 
 |-  B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
22 lcfrlem38.i 
 |-  ( ph -> I e. B )
23 lcfrlem38.n 
 |-  ( ph -> I =/= .0. )
24 lcfrlem38.v 
 |-  V = ( Base ` U )
25 lcfrlem38.t 
 |-  .x. = ( .s ` U )
26 lcfrlem38.s 
 |-  S = ( Scalar ` U )
27 lcfrlem38.r 
 |-  R = ( Base ` S )
28 lcfrlem38.j 
 |-  J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
29 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
30 11 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> ( K e. HL /\ W e. H ) )
31 1 2 3 24 6 7 8 10 11 12 14 lcfrlem4 
 |-  ( ph -> X e. V )
32 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
33 31 17 32 sylanbrc 
 |-  ( ph -> X e. ( V \ { .0. } ) )
34 33 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> X e. ( V \ { .0. } ) )
35 1 2 3 24 6 7 8 10 11 12 15 lcfrlem4 
 |-  ( ph -> Y e. V )
36 eldifsn 
 |-  ( Y e. ( V \ { .0. } ) <-> ( Y e. V /\ Y =/= .0. ) )
37 35 18 36 sylanbrc 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
38 37 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> Y e. ( V \ { .0. } ) )
39 20 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
40 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
41 22 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> I e. B )
42 simpr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> ( ( J ` Y ) ` I ) = ( 0g ` S ) )
43 23 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> I =/= .0. )
44 12 8 eleqtrdi 
 |-  ( ph -> G e. ( LSubSp ` D ) )
45 44 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> G e. ( LSubSp ` D ) )
46 13 9 sseqtrdi 
 |-  ( ph -> G C_ { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
47 46 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> G C_ { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
48 14 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> X e. E )
49 15 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> Y e. E )
50 1 2 3 24 4 16 19 29 30 34 38 39 21 25 26 40 27 28 41 6 7 42 43 45 47 10 48 49 lcfrlem27 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) = ( 0g ` S ) ) -> ( X .+ Y ) e. E )
51 11 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> ( K e. HL /\ W e. H ) )
52 33 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> X e. ( V \ { .0. } ) )
53 37 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> Y e. ( V \ { .0. } ) )
54 20 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
55 22 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> I e. B )
56 simpr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> ( ( J ` Y ) ` I ) =/= ( 0g ` S ) )
57 eqid 
 |-  ( invr ` S ) = ( invr ` S )
58 eqid 
 |-  ( -g ` D ) = ( -g ` D )
59 eqid 
 |-  ( ( J ` X ) ( -g ` D ) ( ( ( ( invr ` S ) ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) ) = ( ( J ` X ) ( -g ` D ) ( ( ( ( invr ` S ) ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )
60 44 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> G e. ( LSubSp ` D ) )
61 46 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> G C_ { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
62 14 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> X e. E )
63 15 adantr 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> Y e. E )
64 1 2 3 24 4 16 19 29 51 52 53 54 21 25 26 40 27 28 55 6 7 56 57 58 59 60 61 10 62 63 lcfrlem37 
 |-  ( ( ph /\ ( ( J ` Y ) ` I ) =/= ( 0g ` S ) ) -> ( X .+ Y ) e. E )
65 50 64 pm2.61dane 
 |-  ( ph -> ( X .+ Y ) e. E )