Metamath Proof Explorer

Theorem hgmapvvlem3

Description: Lemma for hgmapvv . Eliminate ( ( SD )C ) = .1. (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hdmapglem6.h 
|- H = ( LHyp ` K )
hdmapglem6.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapglem6.o 
|- O = ( ( ocH ` K ) ` W )
hdmapglem6.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapglem6.v 
|- V = ( Base ` U )
hdmapglem6.q 
|- .x. = ( .s ` U )
hdmapglem6.r 
|- R = ( Scalar ` U )
hdmapglem6.b 
|- B = ( Base ` R )
hdmapglem6.t 
|- .X. = ( .r ` R )
hdmapglem6.z 
|- .0. = ( 0g ` R )
hdmapglem6.i 
|- .1. = ( 1r ` R )
hdmapglem6.n 
|- N = ( invr ` R )
hdmapglem6.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapglem6.g 
|- G = ( ( HGMap ` K ) ` W )
hdmapglem6.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapglem6.x 
|- ( ph -> X e. ( B \ { .0. } ) )
Assertion hgmapvvlem3 
|- ( ph -> ( G ` ( G ` X ) ) = X )

Proof

Step Hyp Ref Expression
1 hdmapglem6.h 
 |-  H = ( LHyp ` K )
2 hdmapglem6.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapglem6.o 
 |-  O = ( ( ocH ` K ) ` W )
4 hdmapglem6.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 hdmapglem6.v 
 |-  V = ( Base ` U )
6 hdmapglem6.q 
 |-  .x. = ( .s ` U )
7 hdmapglem6.r 
 |-  R = ( Scalar ` U )
8 hdmapglem6.b 
 |-  B = ( Base ` R )
9 hdmapglem6.t 
 |-  .X. = ( .r ` R )
10 hdmapglem6.z 
 |-  .0. = ( 0g ` R )
11 hdmapglem6.i 
 |-  .1. = ( 1r ` R )
12 hdmapglem6.n 
 |-  N = ( invr ` R )
13 hdmapglem6.s 
 |-  S = ( ( HDMap ` K ) ` W )
14 hdmapglem6.g 
 |-  G = ( ( HGMap ` K ) ` W )
15 hdmapglem6.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
16 hdmapglem6.x 
 |-  ( ph -> X e. ( B \ { .0. } ) )
17 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
18 eqid 
 |-  ( Base ` K ) = ( Base ` K )
19 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
20 1 18 19 4 5 17 2 15 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
21 20 eldifad 
 |-  ( ph -> E e. V )
22 1 3 4 5 17 15 21 dochsnnz 
 |-  ( ph -> ( O ` { E } ) =/= { ( 0g ` U ) } )
23 21 snssd 
 |-  ( ph -> { E } C_ V )
24 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
25 1 4 5 24 3 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) e. ( LSubSp ` U ) )
26 15 23 25 syl2anc 
 |-  ( ph -> ( O ` { E } ) e. ( LSubSp ` U ) )
27 17 24 lssne0 
 |-  ( ( O ` { E } ) e. ( LSubSp ` U ) -> ( ( O ` { E } ) =/= { ( 0g ` U ) } <-> E. k e. ( O ` { E } ) k =/= ( 0g ` U ) ) )
28 26 27 syl 
 |-  ( ph -> ( ( O ` { E } ) =/= { ( 0g ` U ) } <-> E. k e. ( O ` { E } ) k =/= ( 0g ` U ) ) )
29 22 28 mpbid 
 |-  ( ph -> E. k e. ( O ` { E } ) k =/= ( 0g ` U ) )
30 eqid 
 |-  ( .s ` U ) = ( .s ` U )
31 15 3ad2ant1 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
32 1 4 5 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
33 15 23 32 syl2anc 
 |-  ( ph -> ( O ` { E } ) C_ V )
34 33 sselda 
 |-  ( ( ph /\ k e. ( O ` { E } ) ) -> k e. V )
35 34 3adant3 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> k e. V )
36 simp3 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> k =/= ( 0g ` U ) )
37 eldifsn 
 |-  ( k e. ( V \ { ( 0g ` U ) } ) <-> ( k e. V /\ k =/= ( 0g ` U ) ) )
38 35 36 37 sylanbrc 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> k e. ( V \ { ( 0g ` U ) } ) )
39 eqid 
 |-  ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) = ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k )
40 1 4 5 30 17 7 11 12 13 31 38 39 hdmapip1 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. )
41 simpl1 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ph )
42 41 15 syl 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( K e. HL /\ W e. H ) )
43 41 16 syl 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> X e. ( B \ { .0. } ) )
44 1 4 15 dvhlmod 
 |-  ( ph -> U e. LMod )
45 41 44 syl 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> U e. LMod )
46 41 26 syl 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( O ` { E } ) e. ( LSubSp ` U ) )
47 1 4 15 dvhlvec 
 |-  ( ph -> U e. LVec )
48 7 lvecdrng 
 |-  ( U e. LVec -> R e. DivRing )
49 47 48 syl 
 |-  ( ph -> R e. DivRing )
50 41 49 syl 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> R e. DivRing )
51 35 adantr 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> k e. V )
52 1 4 5 7 8 13 42 51 51 hdmapipcl 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( ( S ` k ) ` k ) e. B )
53 15 adantr 
 |-  ( ( ph /\ k e. ( O ` { E } ) ) -> ( K e. HL /\ W e. H ) )
54 1 4 5 17 7 10 13 53 34 hdmapip0 
 |-  ( ( ph /\ k e. ( O ` { E } ) ) -> ( ( ( S ` k ) ` k ) = .0. <-> k = ( 0g ` U ) ) )
55 54 necon3bid 
 |-  ( ( ph /\ k e. ( O ` { E } ) ) -> ( ( ( S ` k ) ` k ) =/= .0. <-> k =/= ( 0g ` U ) ) )
56 55 biimp3ar 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> ( ( S ` k ) ` k ) =/= .0. )
57 56 adantr 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( ( S ` k ) ` k ) =/= .0. )
58 8 10 12 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( ( S ` k ) ` k ) e. B /\ ( ( S ` k ) ` k ) =/= .0. ) -> ( N ` ( ( S ` k ) ` k ) ) e. B )
59 50 52 57 58 syl3anc 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( N ` ( ( S ` k ) ` k ) ) e. B )
60 simpl2 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> k e. ( O ` { E } ) )
61 7 30 8 24 lssvscl 
 |-  ( ( ( U e. LMod /\ ( O ` { E } ) e. ( LSubSp ` U ) ) /\ ( ( N ` ( ( S ` k ) ` k ) ) e. B /\ k e. ( O ` { E } ) ) ) -> ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) e. ( O ` { E } ) )
62 45 46 59 60 61 syl22anc 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) e. ( O ` { E } ) )
63 simpr 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. )
64 1 2 3 4 5 6 7 8 9 10 11 12 13 14 42 43 62 60 63 hgmapvvlem2 
 |-  ( ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) /\ ( ( S ` k ) ` ( ( N ` ( ( S ` k ) ` k ) ) ( .s ` U ) k ) ) = .1. ) -> ( G ` ( G ` X ) ) = X )
65 40 64 mpdan 
 |-  ( ( ph /\ k e. ( O ` { E } ) /\ k =/= ( 0g ` U ) ) -> ( G ` ( G ` X ) ) = X )
66 65 rexlimdv3a 
 |-  ( ph -> ( E. k e. ( O ` { E } ) k =/= ( 0g ` U ) -> ( G ` ( G ` X ) ) = X ) )
67 29 66 mpd 
 |-  ( ph -> ( G ` ( G ` X ) ) = X )