Metamath Proof Explorer

Theorem hgmapvvlem2

Description: Lemma for hgmapvv . Eliminate Y (Baer's s). (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. } ) )
hdmapglem6.c 
|- ( ph -> C e. ( O ` { E } ) )
hdmapglem6.d 
|- ( ph -> D e. ( O ` { E } ) )
hdmapglem6.cd 
|- ( ph -> ( ( S ` D ) ` C ) = .1. )
Assertion hgmapvvlem2 
|- ( 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 hdmapglem6.c 
 |-  ( ph -> C e. ( O ` { E } ) )
18 hdmapglem6.d 
 |-  ( ph -> D e. ( O ` { E } ) )
19 hdmapglem6.cd 
 |-  ( ph -> ( ( S ` D ) ` C ) = .1. )
20 1 4 15 dvhlvec 
 |-  ( ph -> U e. LVec )
21 7 lvecdrng 
 |-  ( U e. LVec -> R e. DivRing )
22 20 21 syl 
 |-  ( ph -> R e. DivRing )
23 16 eldifad 
 |-  ( ph -> X e. B )
24 1 4 7 8 14 15 23 hgmapcl 
 |-  ( ph -> ( G ` X ) e. B )
25 eldifsni 
 |-  ( X e. ( B \ { .0. } ) -> X =/= .0. )
26 16 25 syl 
 |-  ( ph -> X =/= .0. )
27 1 4 7 8 10 14 15 23 hgmapeq0 
 |-  ( ph -> ( ( G ` X ) = .0. <-> X = .0. ) )
28 27 necon3bid 
 |-  ( ph -> ( ( G ` X ) =/= .0. <-> X =/= .0. ) )
29 26 28 mpbird 
 |-  ( ph -> ( G ` X ) =/= .0. )
30 8 10 12 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( G ` X ) e. B /\ ( G ` X ) =/= .0. ) -> ( N ` ( G ` X ) ) e. B )
31 22 24 29 30 syl3anc 
 |-  ( ph -> ( N ` ( G ` X ) ) e. B )
32 8 10 12 drnginvrn0 
 |-  ( ( R e. DivRing /\ ( G ` X ) e. B /\ ( G ` X ) =/= .0. ) -> ( N ` ( G ` X ) ) =/= .0. )
33 22 24 29 32 syl3anc 
 |-  ( ph -> ( N ` ( G ` X ) ) =/= .0. )
34 eldifsn 
 |-  ( ( N ` ( G ` X ) ) e. ( B \ { .0. } ) <-> ( ( N ` ( G ` X ) ) e. B /\ ( N ` ( G ` X ) ) =/= .0. ) )
35 31 33 34 sylanbrc 
 |-  ( ph -> ( N ` ( G ` X ) ) e. ( B \ { .0. } ) )
36 8 10 9 11 12 drnginvrl 
 |-  ( ( R e. DivRing /\ ( G ` X ) e. B /\ ( G ` X ) =/= .0. ) -> ( ( N ` ( G ` X ) ) .X. ( G ` X ) ) = .1. )
37 22 24 29 36 syl3anc 
 |-  ( ph -> ( ( N ` ( G ` X ) ) .X. ( G ` X ) ) = .1. )
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 35 37 hgmapvvlem1 
 |-  ( ph -> ( G ` ( G ` X ) ) = X )