Metamath Proof Explorer

Theorem hgmapvv

Description: Value of a double involution. Part 1.2 of Baer p. 110 line 37. (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hgmapvv.h 
|- H = ( LHyp ` K )
hgmapvv.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapvv.r 
|- R = ( Scalar ` U )
hgmapvv.b 
|- B = ( Base ` R )
hgmapvv.g 
|- G = ( ( HGMap ` K ) ` W )
hgmapvv.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hgmapvv.j 
|- ( ph -> X e. B )
Assertion hgmapvv 
|- ( ph -> ( G ` ( G ` X ) ) = X )

Proof

Step Hyp Ref Expression
1 hgmapvv.h 
 |-  H = ( LHyp ` K )
2 hgmapvv.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapvv.r 
 |-  R = ( Scalar ` U )
4 hgmapvv.b 
 |-  B = ( Base ` R )
5 hgmapvv.g 
 |-  G = ( ( HGMap ` K ) ` W )
6 hgmapvv.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 hgmapvv.j 
 |-  ( ph -> X e. B )
8 2fveq3 
 |-  ( X = ( 0g ` R ) -> ( G ` ( G ` X ) ) = ( G ` ( G ` ( 0g ` R ) ) ) )
9 id 
 |-  ( X = ( 0g ` R ) -> X = ( 0g ` R ) )
10 8 9 eqeq12d 
 |-  ( X = ( 0g ` R ) -> ( ( G ` ( G ` X ) ) = X <-> ( G ` ( G ` ( 0g ` R ) ) ) = ( 0g ` R ) ) )
11 eqid 
 |-  <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
12 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
13 eqid 
 |-  ( Base ` U ) = ( Base ` U )
14 eqid 
 |-  ( .s ` U ) = ( .s ` U )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
18 eqid 
 |-  ( invr ` R ) = ( invr ` R )
19 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
20 6 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( K e. HL /\ W e. H ) )
21 7 anim1i 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( X e. B /\ X =/= ( 0g ` R ) ) )
22 eldifsn 
 |-  ( X e. ( B \ { ( 0g ` R ) } ) <-> ( X e. B /\ X =/= ( 0g ` R ) ) )
23 21 22 sylibr 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> X e. ( B \ { ( 0g ` R ) } ) )
24 1 11 12 2 13 14 3 4 15 16 17 18 19 5 20 23 hgmapvvlem3 
 |-  ( ( ph /\ X =/= ( 0g ` R ) ) -> ( G ` ( G ` X ) ) = X )
25 1 2 3 16 5 6 hgmapval0 
 |-  ( ph -> ( G ` ( 0g ` R ) ) = ( 0g ` R ) )
26 25 fveq2d 
 |-  ( ph -> ( G ` ( G ` ( 0g ` R ) ) ) = ( G ` ( 0g ` R ) ) )
27 26 25 eqtrd 
 |-  ( ph -> ( G ` ( G ` ( 0g ` R ) ) ) = ( 0g ` R ) )
28 10 24 27 pm2.61ne 
 |-  ( ph -> ( G ` ( G ` X ) ) = X )