Metamath Proof Explorer

Theorem lclkrlem2y

Description: Lemma for lclkr . Restate the hypotheses for E and G to say their kernels are closed, in order to eliminate the generating vectors X and Y . (Contributed by NM, 18-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lclkrlem2y.l 
 |-  L = ( LKer ` U )
2 lclkrlem2y.h 
 |-  H = ( LHyp ` K )
3 lclkrlem2y.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
4 lclkrlem2y.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 lclkrlem2y.f 
 |-  F = ( LFnl ` U )
6 lclkrlem2y.d 
 |-  D = ( LDual ` U )
7 lclkrlem2y.p 
 |-  .+ = ( +g ` D )
8 lclkrlem2y.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 lclkrlem2y.e 
 |-  ( ph -> E e. F )
10 lclkrlem2y.g 
 |-  ( ph -> G e. F )
11 lclkrlem2y.le 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) )
12 lclkrlem2y.lg 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
13 eqid 
 |-  ( Base ` U ) = ( Base ` U )
14 2 3 4 13 5 1 8 10 lcfl8a 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> E. y e. ( Base ` U ) ( L ` G ) = ( ._|_ ` { y } ) ) )
15 12 14 mpbid 
 |-  ( ph -> E. y e. ( Base ` U ) ( L ` G ) = ( ._|_ ` { y } ) )
16 2 3 4 13 5 1 8 9 lcfl8a 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) <-> E. x e. ( Base ` U ) ( L ` E ) = ( ._|_ ` { x } ) ) )
17 11 16 mpbid 
 |-  ( ph -> E. x e. ( Base ` U ) ( L ` E ) = ( ._|_ ` { x } ) )
18 8 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> ( K e. HL /\ W e. H ) )
19 simp21 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> x e. ( Base ` U ) )
20 simp23 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> y e. ( Base ` U ) )
21 9 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> E e. F )
22 10 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> G e. F )
23 simp22 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> ( L ` E ) = ( ._|_ ` { x } ) )
24 simp3 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> ( L ` G ) = ( ._|_ ` { y } ) )
25 1 2 3 4 13 5 6 7 18 19 20 21 22 23 24 lclkrlem2x 
 |-  ( ( ph /\ ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) /\ ( L ` G ) = ( ._|_ ` { y } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
26 25 3exp 
 |-  ( ph -> ( ( x e. ( Base ` U ) /\ ( L ` E ) = ( ._|_ ` { x } ) /\ y e. ( Base ` U ) ) -> ( ( L ` G ) = ( ._|_ ` { y } ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) ) )
27 26 3expd 
 |-  ( ph -> ( x e. ( Base ` U ) -> ( ( L ` E ) = ( ._|_ ` { x } ) -> ( y e. ( Base ` U ) -> ( ( L ` G ) = ( ._|_ ` { y } ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) ) ) ) )
28 27 rexlimdv 
 |-  ( ph -> ( E. x e. ( Base ` U ) ( L ` E ) = ( ._|_ ` { x } ) -> ( y e. ( Base ` U ) -> ( ( L ` G ) = ( ._|_ ` { y } ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) ) ) )
29 17 28 mpd 
 |-  ( ph -> ( y e. ( Base ` U ) -> ( ( L ` G ) = ( ._|_ ` { y } ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) ) )
30 29 rexlimdv 
 |-  ( ph -> ( E. y e. ( Base ` U ) ( L ` G ) = ( ._|_ ` { y } ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) )
31 15 30 mpd 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )