Metamath Proof Explorer

Theorem lcfrlem20

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

Ref Expression
Hypotheses lcfrlem17.h 
|- H = ( LHyp ` K )
lcfrlem17.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfrlem17.u 
|- U = ( ( DVecH ` K ) ` W )
lcfrlem17.v 
|- V = ( Base ` U )
lcfrlem17.p 
|- .+ = ( +g ` U )
lcfrlem17.z 
|- .0. = ( 0g ` U )
lcfrlem17.n 
|- N = ( LSpan ` U )
lcfrlem17.a 
|- A = ( LSAtoms ` U )
lcfrlem17.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrlem17.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lcfrlem17.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
lcfrlem17.ne 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
lcfrlem20.e 
|- ( ph -> -. X e. ( ._|_ ` { ( X .+ Y ) } ) )
Assertion lcfrlem20 
|- ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )

Proof

Step Hyp Ref Expression
1 lcfrlem17.h 
 |-  H = ( LHyp ` K )
2 lcfrlem17.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfrlem17.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfrlem17.v 
 |-  V = ( Base ` U )
5 lcfrlem17.p 
 |-  .+ = ( +g ` U )
6 lcfrlem17.z 
 |-  .0. = ( 0g ` U )
7 lcfrlem17.n 
 |-  N = ( LSpan ` U )
8 lcfrlem17.a 
 |-  A = ( LSAtoms ` U )
9 lcfrlem17.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcfrlem17.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
11 lcfrlem17.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
12 lcfrlem17.ne 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
13 lcfrlem20.e 
 |-  ( ph -> -. X e. ( ._|_ ` { ( X .+ Y ) } ) )
14 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
15 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
16 10 eldifad 
 |-  ( ph -> X e. V )
17 11 eldifad 
 |-  ( ph -> Y e. V )
18 4 7 14 15 16 17 lsmpr 
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) )
19 18 ineq1d 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) = ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) )
20 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
21 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
22 1 3 9 dvhlvec 
 |-  ( ph -> U e. LVec )
23 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem17 
 |-  ( ph -> ( X .+ Y ) e. ( V \ { .0. } ) )
24 1 2 3 4 6 21 9 23 dochsnshp 
 |-  ( ph -> ( ._|_ ` { ( X .+ Y ) } ) e. ( LSHyp ` U ) )
25 4 7 6 8 15 10 lsatlspsn 
 |-  ( ph -> ( N ` { X } ) e. A )
26 4 7 6 8 15 11 lsatlspsn 
 |-  ( ph -> ( N ` { Y } ) e. A )
27 4 5 lmodvacl 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
28 15 16 17 27 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. V )
29 28 snssd 
 |-  ( ph -> { ( X .+ Y ) } C_ V )
30 1 3 4 20 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { ( X .+ Y ) } C_ V ) -> ( ._|_ ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) )
31 9 29 30 syl2anc 
 |-  ( ph -> ( ._|_ ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) )
32 4 20 7 15 31 16 lspsnel5 
 |-  ( ph -> ( X e. ( ._|_ ` { ( X .+ Y ) } ) <-> ( N ` { X } ) C_ ( ._|_ ` { ( X .+ Y ) } ) ) )
33 13 32 mtbid 
 |-  ( ph -> -. ( N ` { X } ) C_ ( ._|_ ` { ( X .+ Y ) } ) )
34 20 14 21 8 22 24 25 26 12 33 lshpat 
 |-  ( ph -> ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )
35 19 34 eqeltrd 
 |-  ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. A )