Metamath Proof Explorer

Theorem lclkrlem2b

Description: Lemma for lclkr . (Contributed by NM, 17-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lclkrlem2a.h 
 |-  H = ( LHyp ` K )
2 lclkrlem2a.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lclkrlem2a.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lclkrlem2a.v 
 |-  V = ( Base ` U )
5 lclkrlem2a.z 
 |-  .0. = ( 0g ` U )
6 lclkrlem2a.p 
 |-  .(+) = ( LSSum ` U )
7 lclkrlem2a.n 
 |-  N = ( LSpan ` U )
8 lclkrlem2a.a 
 |-  A = ( LSAtoms ` U )
9 lclkrlem2a.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lclkrlem2a.b 
 |-  ( ph -> B e. ( V \ { .0. } ) )
11 lclkrlem2a.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
12 lclkrlem2a.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
13 lclkrlem2a.e 
 |-  ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )
14 lclkrlem2b.da 
 |-  ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
15 9 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> ( K e. HL /\ W e. H ) )
16 10 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> B e. ( V \ { .0. } ) )
17 11 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> X e. ( V \ { .0. } ) )
18 12 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> Y e. ( V \ { .0. } ) )
19 13 adantr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )
20 simpr 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> -. X e. ( ._|_ ` { B } ) )
21 1 2 3 4 5 6 7 8 15 16 17 18 19 20 lclkrlem2a 
 |-  ( ( ph /\ -. X e. ( ._|_ ` { B } ) ) -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
22 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
23 lmodabl 
 |-  ( U e. LMod -> U e. Abel )
24 22 23 syl 
 |-  ( ph -> U e. Abel )
25 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
26 25 lsssssubg 
 |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
27 22 26 syl 
 |-  ( ph -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
28 11 eldifad 
 |-  ( ph -> X e. V )
29 4 25 7 lspsncl 
 |-  ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
30 22 28 29 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` U ) )
31 27 30 sseldd 
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` U ) )
32 12 eldifad 
 |-  ( ph -> Y e. V )
33 4 25 7 lspsncl 
 |-  ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )
34 22 32 33 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )
35 27 34 sseldd 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` U ) )
36 6 lsmcom 
 |-  ( ( U e. Abel /\ ( N ` { X } ) e. ( SubGrp ` U ) /\ ( N ` { Y } ) e. ( SubGrp ` U ) ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( ( N ` { Y } ) .(+) ( N ` { X } ) ) )
37 24 31 35 36 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( ( N ` { Y } ) .(+) ( N ` { X } ) ) )
38 37 ineq1d 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) = ( ( ( N ` { Y } ) .(+) ( N ` { X } ) ) i^i ( ._|_ ` { B } ) ) )
39 38 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) = ( ( ( N ` { Y } ) .(+) ( N ` { X } ) ) i^i ( ._|_ ` { B } ) ) )
40 9 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> ( K e. HL /\ W e. H ) )
41 10 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> B e. ( V \ { .0. } ) )
42 12 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> Y e. ( V \ { .0. } ) )
43 11 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> X e. ( V \ { .0. } ) )
44 13 necomd 
 |-  ( ph -> ( ._|_ ` { Y } ) =/= ( ._|_ ` { X } ) )
45 44 adantr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> ( ._|_ ` { Y } ) =/= ( ._|_ ` { X } ) )
46 simpr 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> -. Y e. ( ._|_ ` { B } ) )
47 1 2 3 4 5 6 7 8 40 41 42 43 45 46 lclkrlem2a 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> ( ( ( N ` { Y } ) .(+) ( N ` { X } ) ) i^i ( ._|_ ` { B } ) ) e. A )
48 39 47 eqeltrd 
 |-  ( ( ph /\ -. Y e. ( ._|_ ` { B } ) ) -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
49 21 48 14 mpjaodan 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )