Metamath Proof Explorer

Theorem hdmapglem5

Description: Part 1.2 in Baer p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hdmapglem5.h 
|- H = ( LHyp ` K )
hdmapglem5.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapglem5.o 
|- O = ( ( ocH ` K ) ` W )
hdmapglem5.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapglem5.v 
|- V = ( Base ` U )
hdmapglem5.p 
|- .+ = ( +g ` U )
hdmapglem5.m 
|- .- = ( -g ` U )
hdmapglem5.q 
|- .x. = ( .s ` U )
hdmapglem5.r 
|- R = ( Scalar ` U )
hdmapglem5.b 
|- B = ( Base ` R )
hdmapglem5.t 
|- .X. = ( .r ` R )
hdmapglem5.z 
|- .0. = ( 0g ` R )
hdmapglem5.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapglem5.g 
|- G = ( ( HGMap ` K ) ` W )
hdmapglem5.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapglem5.c 
|- ( ph -> C e. ( O ` { E } ) )
hdmapglem5.d 
|- ( ph -> D e. ( O ` { E } ) )
hdmapglem5.i 
|- ( ph -> I e. B )
hdmapglem5.j 
|- ( ph -> J e. B )
Assertion hdmapglem5 
|- ( ph -> ( G ` ( ( S ` D ) ` C ) ) = ( ( S ` C ) ` D ) )

Proof

Step Hyp Ref Expression
1 hdmapglem5.h 
 |-  H = ( LHyp ` K )
2 hdmapglem5.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapglem5.o 
 |-  O = ( ( ocH ` K ) ` W )
4 hdmapglem5.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 hdmapglem5.v 
 |-  V = ( Base ` U )
6 hdmapglem5.p 
 |-  .+ = ( +g ` U )
7 hdmapglem5.m 
 |-  .- = ( -g ` U )
8 hdmapglem5.q 
 |-  .x. = ( .s ` U )
9 hdmapglem5.r 
 |-  R = ( Scalar ` U )
10 hdmapglem5.b 
 |-  B = ( Base ` R )
11 hdmapglem5.t 
 |-  .X. = ( .r ` R )
12 hdmapglem5.z 
 |-  .0. = ( 0g ` R )
13 hdmapglem5.s 
 |-  S = ( ( HDMap ` K ) ` W )
14 hdmapglem5.g 
 |-  G = ( ( HGMap ` K ) ` W )
15 hdmapglem5.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
16 hdmapglem5.c 
 |-  ( ph -> C e. ( O ` { E } ) )
17 hdmapglem5.d 
 |-  ( ph -> D e. ( O ` { E } ) )
18 hdmapglem5.i 
 |-  ( ph -> I e. B )
19 hdmapglem5.j 
 |-  ( ph -> J e. B )
20 1 4 15 dvhlmod 
 |-  ( ph -> U e. LMod )
21 9 lmodring 
 |-  ( U e. LMod -> R e. Ring )
22 20 21 syl 
 |-  ( ph -> R e. Ring )
23 eqid 
 |-  ( Base ` K ) = ( Base ` K )
24 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
25 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
26 1 23 24 4 5 25 2 15 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
27 26 eldifad 
 |-  ( ph -> E e. V )
28 27 snssd 
 |-  ( ph -> { E } C_ V )
29 1 4 5 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
30 15 28 29 syl2anc 
 |-  ( ph -> ( O ` { E } ) C_ V )
31 30 16 sseldd 
 |-  ( ph -> C e. V )
32 30 17 sseldd 
 |-  ( ph -> D e. V )
33 1 4 5 9 10 13 15 31 32 hdmapipcl 
 |-  ( ph -> ( ( S ` D ) ` C ) e. B )
34 1 4 9 10 14 15 33 hgmapcl 
 |-  ( ph -> ( G ` ( ( S ` D ) ` C ) ) e. B )
35 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
36 10 11 35 ringlidm 
 |-  ( ( R e. Ring /\ ( G ` ( ( S ` D ) ` C ) ) e. B ) -> ( ( 1r ` R ) .X. ( G ` ( ( S ` D ) ` C ) ) ) = ( G ` ( ( S ` D ) ` C ) ) )
37 22 34 36 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) .X. ( G ` ( ( S ` D ) ` C ) ) ) = ( G ` ( ( S ` D ) ` C ) ) )
38 10 35 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
39 22 38 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
40 1 4 9 35 14 15 hgmapval1 
 |-  ( ph -> ( G ` ( 1r ` R ) ) = ( 1r ` R ) )
41 40 oveq2d 
 |-  ( ph -> ( ( ( S ` D ) ` C ) .X. ( G ` ( 1r ` R ) ) ) = ( ( ( S ` D ) ` C ) .X. ( 1r ` R ) ) )
42 10 11 35 ringridm 
 |-  ( ( R e. Ring /\ ( ( S ` D ) ` C ) e. B ) -> ( ( ( S ` D ) ` C ) .X. ( 1r ` R ) ) = ( ( S ` D ) ` C ) )
43 22 33 42 syl2anc 
 |-  ( ph -> ( ( ( S ` D ) ` C ) .X. ( 1r ` R ) ) = ( ( S ` D ) ` C ) )
44 41 43 eqtrd 
 |-  ( ph -> ( ( ( S ` D ) ` C ) .X. ( G ` ( 1r ` R ) ) ) = ( ( S ` D ) ` C ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 33 39 44 hdmapinvlem4 
 |-  ( ph -> ( ( 1r ` R ) .X. ( G ` ( ( S ` D ) ` C ) ) ) = ( ( S ` C ) ` D ) )
46 37 45 eqtr3d 
 |-  ( ph -> ( G ` ( ( S ` D ) ` C ) ) = ( ( S ` C ) ` D ) )