Metamath Proof Explorer

Theorem lclkrlem2x

Description: Lemma for lclkr . Eliminate by cases the hypotheses of lclkrlem2u , lclkrlem2u and lclkrlem2w . (Contributed by NM, 18-Jan-2015)

Ref Expression
Hypotheses lclkrlem2x.l 
|- L = ( LKer ` U )
lclkrlem2x.h 
|- H = ( LHyp ` K )
lclkrlem2x.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem2x.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrlem2x.v 
|- V = ( Base ` U )
lclkrlem2x.f 
|- F = ( LFnl ` U )
lclkrlem2x.d 
|- D = ( LDual ` U )
lclkrlem2x.p 
|- .+ = ( +g ` D )
lclkrlem2x.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem2x.x 
|- ( ph -> X e. V )
lclkrlem2x.y 
|- ( ph -> Y e. V )
lclkrlem2x.e 
|- ( ph -> E e. F )
lclkrlem2x.g 
|- ( ph -> G e. F )
lclkrlem2x.le 
|- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
lclkrlem2x.lg 
|- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
Assertion lclkrlem2x 
|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2x.l 
 |-  L = ( LKer ` U )
2 lclkrlem2x.h 
 |-  H = ( LHyp ` K )
3 lclkrlem2x.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
4 lclkrlem2x.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 lclkrlem2x.v 
 |-  V = ( Base ` U )
6 lclkrlem2x.f 
 |-  F = ( LFnl ` U )
7 lclkrlem2x.d 
 |-  D = ( LDual ` U )
8 lclkrlem2x.p 
 |-  .+ = ( +g ` D )
9 lclkrlem2x.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lclkrlem2x.x 
 |-  ( ph -> X e. V )
11 lclkrlem2x.y 
 |-  ( ph -> Y e. V )
12 lclkrlem2x.e 
 |-  ( ph -> E e. F )
13 lclkrlem2x.g 
 |-  ( ph -> G e. F )
14 lclkrlem2x.le 
 |-  ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
15 lclkrlem2x.lg 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
16 df-ne 
 |-  ( ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) <-> -. ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) )
17 eqid 
 |-  ( .s ` U ) = ( .s ` U )
18 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
19 eqid 
 |-  ( .r ` ( Scalar ` U ) ) = ( .r ` ( Scalar ` U ) )
20 eqid 
 |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
21 eqid 
 |-  ( invr ` ( Scalar ` U ) ) = ( invr ` ( Scalar ` U ) )
22 eqid 
 |-  ( -g ` U ) = ( -g ` U )
23 10 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> X e. V )
24 11 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> Y e. V )
25 12 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> E e. F )
26 13 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> G e. F )
27 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
28 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
29 9 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( K e. HL /\ W e. H ) )
30 14 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( L ` E ) = ( ._|_ ` { X } ) )
31 15 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( L ` G ) = ( ._|_ ` { Y } ) )
32 simpr 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) )
33 5 17 18 19 20 21 22 6 7 8 23 24 25 26 27 1 2 3 4 28 29 30 31 32 lclkrlem2u 
 |-  ( ( ph /\ ( ( E .+ G ) ` X ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
34 16 33 sylan2br 
 |-  ( ( ph /\ -. ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
35 df-ne 
 |-  ( ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) <-> -. ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) )
36 10 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> X e. V )
37 11 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> Y e. V )
38 12 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> E e. F )
39 13 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> G e. F )
40 9 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( K e. HL /\ W e. H ) )
41 14 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( L ` E ) = ( ._|_ ` { X } ) )
42 15 adantr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( L ` G ) = ( ._|_ ` { Y } ) )
43 simpr 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) )
44 5 17 18 19 20 21 22 6 7 8 36 37 38 39 27 1 2 3 4 28 40 41 42 43 lclkrlem2t 
 |-  ( ( ph /\ ( ( E .+ G ) ` Y ) =/= ( 0g ` ( Scalar ` U ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
45 35 44 sylan2br 
 |-  ( ( ph /\ -. ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
46 10 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> X e. V )
47 11 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> Y e. V )
48 12 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> E e. F )
49 13 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> G e. F )
50 9 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> ( K e. HL /\ W e. H ) )
51 14 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> ( L ` E ) = ( ._|_ ` { X } ) )
52 15 adantr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> ( L ` G ) = ( ._|_ ` { Y } ) )
53 simprl 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) )
54 simprr 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) )
55 5 17 18 19 20 21 22 6 7 8 46 47 48 49 27 1 2 3 4 28 50 51 52 53 54 lclkrlem2w 
 |-  ( ( ph /\ ( ( ( E .+ G ) ` X ) = ( 0g ` ( Scalar ` U ) ) /\ ( ( E .+ G ) ` Y ) = ( 0g ` ( Scalar ` U ) ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
56 34 45 55 pm2.61dda 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )