Metamath Proof Explorer

Theorem hgmapvvlem1

Description: Involution property of scalar sigma map. Line 10 in Baer p. 111, t sigma squared = t. Our E , C , D , Y , X correspond to Baer's w, h, k, s, t. (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. )
hdmapglem6.y 
|- ( ph -> Y e. ( B \ { .0. } ) )
hdmapglem6.yx 
|- ( ph -> ( Y .X. ( G ` X ) ) = .1. )
Assertion hgmapvvlem1 
|- ( 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 hdmapglem6.y 
 |-  ( ph -> Y e. ( B \ { .0. } ) )
21 hdmapglem6.yx 
 |-  ( ph -> ( Y .X. ( G ` X ) ) = .1. )
22 1 4 15 dvhlmod 
 |-  ( ph -> U e. LMod )
23 7 lmodring 
 |-  ( U e. LMod -> R e. Ring )
24 22 23 syl 
 |-  ( ph -> R e. Ring )
25 16 eldifad 
 |-  ( ph -> X e. B )
26 1 4 7 8 14 15 25 hgmapcl 
 |-  ( ph -> ( G ` X ) e. B )
27 1 4 7 8 14 15 26 hgmapcl 
 |-  ( ph -> ( G ` ( G ` X ) ) e. B )
28 20 eldifad 
 |-  ( ph -> Y e. B )
29 1 4 7 8 14 15 28 hgmapcl 
 |-  ( ph -> ( G ` Y ) e. B )
30 1 4 15 dvhlvec 
 |-  ( ph -> U e. LVec )
31 7 lvecdrng 
 |-  ( U e. LVec -> R e. DivRing )
32 30 31 syl 
 |-  ( ph -> R e. DivRing )
33 eldifsni 
 |-  ( Y e. ( B \ { .0. } ) -> Y =/= .0. )
34 20 33 syl 
 |-  ( ph -> Y =/= .0. )
35 1 4 7 8 10 14 15 28 hgmapeq0 
 |-  ( ph -> ( ( G ` Y ) = .0. <-> Y = .0. ) )
36 35 necon3bid 
 |-  ( ph -> ( ( G ` Y ) =/= .0. <-> Y =/= .0. ) )
37 34 36 mpbird 
 |-  ( ph -> ( G ` Y ) =/= .0. )
38 8 10 12 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( G ` Y ) e. B /\ ( G ` Y ) =/= .0. ) -> ( N ` ( G ` Y ) ) e. B )
39 32 29 37 38 syl3anc 
 |-  ( ph -> ( N ` ( G ` Y ) ) e. B )
40 8 9 ringass 
 |-  ( ( R e. Ring /\ ( ( G ` ( G ` X ) ) e. B /\ ( G ` Y ) e. B /\ ( N ` ( G ` Y ) ) e. B ) ) -> ( ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) = ( ( G ` ( G ` X ) ) .X. ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) ) )
41 24 27 29 39 40 syl13anc 
 |-  ( ph -> ( ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) = ( ( G ` ( G ` X ) ) .X. ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) ) )
42 8 10 9 11 12 drnginvrr 
 |-  ( ( R e. DivRing /\ ( G ` Y ) e. B /\ ( G ` Y ) =/= .0. ) -> ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) = .1. )
43 32 29 37 42 syl3anc 
 |-  ( ph -> ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) = .1. )
44 43 oveq2d 
 |-  ( ph -> ( ( G ` ( G ` X ) ) .X. ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) ) = ( ( G ` ( G ` X ) ) .X. .1. ) )
45 8 9 11 ringridm 
 |-  ( ( R e. Ring /\ ( G ` ( G ` X ) ) e. B ) -> ( ( G ` ( G ` X ) ) .X. .1. ) = ( G ` ( G ` X ) ) )
46 24 27 45 syl2anc 
 |-  ( ph -> ( ( G ` ( G ` X ) ) .X. .1. ) = ( G ` ( G ` X ) ) )
47 41 44 46 3eqtrrd 
 |-  ( ph -> ( G ` ( G ` X ) ) = ( ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) )
48 21 fveq2d 
 |-  ( ph -> ( G ` ( Y .X. ( G ` X ) ) ) = ( G ` .1. ) )
49 1 4 7 8 9 14 15 28 26 hgmapmul 
 |-  ( ph -> ( G ` ( Y .X. ( G ` X ) ) ) = ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) )
50 48 49 eqtr3d 
 |-  ( ph -> ( G ` .1. ) = ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) )
51 19 fveq2d 
 |-  ( ph -> ( G ` ( ( S ` D ) ` C ) ) = ( G ` .1. ) )
52 eqid 
 |-  ( +g ` U ) = ( +g ` U )
53 eqid 
 |-  ( -g ` U ) = ( -g ` U )
54 1 2 3 4 5 52 53 6 7 8 9 10 13 14 15 17 18 28 25 hdmapglem5 
 |-  ( ph -> ( G ` ( ( S ` D ) ` C ) ) = ( ( S ` C ) ` D ) )
55 51 54 eqtr3d 
 |-  ( ph -> ( G ` .1. ) = ( ( S ` C ) ` D ) )
56 50 55 eqtr3d 
 |-  ( ph -> ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) = ( ( S ` C ) ` D ) )
57 21 19 eqtr4d 
 |-  ( ph -> ( Y .X. ( G ` X ) ) = ( ( S ` D ) ` C ) )
58 1 2 3 4 5 52 53 6 7 8 9 10 13 14 15 17 18 28 25 57 hdmapinvlem4 
 |-  ( ph -> ( X .X. ( G ` Y ) ) = ( ( S ` C ) ` D ) )
59 56 58 eqtr4d 
 |-  ( ph -> ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) = ( X .X. ( G ` Y ) ) )
60 59 oveq1d 
 |-  ( ph -> ( ( ( G ` ( G ` X ) ) .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) = ( ( X .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) )
61 8 9 ringass 
 |-  ( ( R e. Ring /\ ( X e. B /\ ( G ` Y ) e. B /\ ( N ` ( G ` Y ) ) e. B ) ) -> ( ( X .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) = ( X .X. ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) ) )
62 24 25 29 39 61 syl13anc 
 |-  ( ph -> ( ( X .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) = ( X .X. ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) ) )
63 43 oveq2d 
 |-  ( ph -> ( X .X. ( ( G ` Y ) .X. ( N ` ( G ` Y ) ) ) ) = ( X .X. .1. ) )
64 8 9 11 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .X. .1. ) = X )
65 24 25 64 syl2anc 
 |-  ( ph -> ( X .X. .1. ) = X )
66 62 63 65 3eqtrd 
 |-  ( ph -> ( ( X .X. ( G ` Y ) ) .X. ( N ` ( G ` Y ) ) ) = X )
67 47 60 66 3eqtrd 
 |-  ( ph -> ( G ` ( G ` X ) ) = X )