Metamath Proof Explorer

Theorem hdmapglem7

Description: Lemma for hdmapg . Line 15 in Baer p. 111, f(x,y) alpha = f(y,x). In the proof, our E , ( O{ E } ) , X , Y , k , u , l , and v correspond respectively to Baer's w, H, x, y, x', x'', y', and y'', and our ( ( SY )X ) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapglem7.h 
|- H = ( LHyp ` K )
hdmapglem7.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapglem7.o 
|- O = ( ( ocH ` K ) ` W )
hdmapglem7.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapglem7.v 
|- V = ( Base ` U )
hdmapglem7.p 
|- .+ = ( +g ` U )
hdmapglem7.q 
|- .x. = ( .s ` U )
hdmapglem7.r 
|- R = ( Scalar ` U )
hdmapglem7.b 
|- B = ( Base ` R )
hdmapglem7.a 
|- .(+) = ( LSSum ` U )
hdmapglem7.n 
|- N = ( LSpan ` U )
hdmapglem7.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapglem7.x 
|- ( ph -> X e. V )
hdmapglem7.t 
|- .X. = ( .r ` R )
hdmapglem7.z 
|- .0. = ( 0g ` R )
hdmapglem7.c 
|- .+b = ( +g ` R )
hdmapglem7.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapglem7.g 
|- G = ( ( HGMap ` K ) ` W )
hdmapglem7.y 
|- ( ph -> Y e. V )
Assertion hdmapglem7 
|- ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )

Proof

Step Hyp Ref Expression
1 hdmapglem7.h 
 |-  H = ( LHyp ` K )
2 hdmapglem7.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapglem7.o 
 |-  O = ( ( ocH ` K ) ` W )
4 hdmapglem7.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 hdmapglem7.v 
 |-  V = ( Base ` U )
6 hdmapglem7.p 
 |-  .+ = ( +g ` U )
7 hdmapglem7.q 
 |-  .x. = ( .s ` U )
8 hdmapglem7.r 
 |-  R = ( Scalar ` U )
9 hdmapglem7.b 
 |-  B = ( Base ` R )
10 hdmapglem7.a 
 |-  .(+) = ( LSSum ` U )
11 hdmapglem7.n 
 |-  N = ( LSpan ` U )
12 hdmapglem7.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 hdmapglem7.x 
 |-  ( ph -> X e. V )
14 hdmapglem7.t 
 |-  .X. = ( .r ` R )
15 hdmapglem7.z 
 |-  .0. = ( 0g ` R )
16 hdmapglem7.c 
 |-  .+b = ( +g ` R )
17 hdmapglem7.s 
 |-  S = ( ( HDMap ` K ) ` W )
18 hdmapglem7.g 
 |-  G = ( ( HGMap ` K ) ` W )
19 hdmapglem7.y 
 |-  ( ph -> Y e. V )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 hdmapglem7a 
 |-  ( ph -> E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 19 hdmapglem7a 
 |-  ( ph -> E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) )
22 12 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( K e. HL /\ W e. H ) )
23 1 4 12 dvhlmod 
 |-  ( ph -> U e. LMod )
24 8 lmodring 
 |-  ( U e. LMod -> R e. Ring )
25 23 24 syl 
 |-  ( ph -> R e. Ring )
26 25 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> R e. Ring )
27 simplrr 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> k e. B )
28 simprr 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> l e. B )
29 1 4 8 9 18 22 28 hgmapcl 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` l ) e. B )
30 9 14 ringcl 
 |-  ( ( R e. Ring /\ k e. B /\ ( G ` l ) e. B ) -> ( k .X. ( G ` l ) ) e. B )
31 26 27 29 30 syl3anc 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( k .X. ( G ` l ) ) e. B )
32 eqid 
 |-  ( Base ` K ) = ( Base ` K )
33 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
34 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
35 1 32 33 4 5 34 2 12 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
36 35 eldifad 
 |-  ( ph -> E e. V )
37 36 snssd 
 |-  ( ph -> { E } C_ V )
38 1 4 5 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
39 12 37 38 syl2anc 
 |-  ( ph -> ( O ` { E } ) C_ V )
40 39 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( O ` { E } ) C_ V )
41 simplrl 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> u e. ( O ` { E } ) )
42 40 41 sseldd 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> u e. V )
43 simprl 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> v e. ( O ` { E } ) )
44 40 43 sseldd 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> v e. V )
45 1 4 5 8 9 17 22 42 44 hdmapipcl 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( S ` v ) ` u ) e. B )
46 1 4 8 9 16 18 22 31 45 hgmapadd 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) = ( ( G ` ( k .X. ( G ` l ) ) ) .+b ( G ` ( ( S ` v ) ` u ) ) ) )
47 1 4 8 9 14 18 22 27 29 hgmapmul 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( k .X. ( G ` l ) ) ) = ( ( G ` ( G ` l ) ) .X. ( G ` k ) ) )
48 1 4 8 9 18 22 28 hgmapvv 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( G ` l ) ) = l )
49 48 oveq1d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( G ` ( G ` l ) ) .X. ( G ` k ) ) = ( l .X. ( G ` k ) ) )
50 47 49 eqtrd 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( k .X. ( G ` l ) ) ) = ( l .X. ( G ` k ) ) )
51 eqid 
 |-  ( -g ` U ) = ( -g ` U )
52 1 2 3 4 5 6 51 7 8 9 14 15 17 18 22 41 43 27 27 hdmapglem5 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` v ) ` u ) ) = ( ( S ` u ) ` v ) )
53 50 52 oveq12d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( G ` ( k .X. ( G ` l ) ) ) .+b ( G ` ( ( S ` v ) ` u ) ) ) = ( ( l .X. ( G ` k ) ) .+b ( ( S ` u ) ` v ) ) )
54 46 53 eqtrd 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) = ( ( l .X. ( G ` k ) ) .+b ( ( S ` u ) ` v ) ) )
55 13 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> X e. V )
56 1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 43 41 28 27 hdmapglem7b 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) = ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) )
57 56 fveq2d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( G ` ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) )
58 1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 41 43 27 28 hdmapglem7b 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) = ( ( l .X. ( G ` k ) ) .+b ( ( S ` u ) ` v ) ) )
59 54 57 58 3eqtr4d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) )
60 59 3adantl3 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) )
61 60 3adant3 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) )
62 simp3 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> Y = ( ( l .x. E ) .+ v ) )
63 62 fveq2d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( S ` Y ) = ( S ` ( ( l .x. E ) .+ v ) ) )
64 simp13 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> X = ( ( k .x. E ) .+ u ) )
65 63 64 fveq12d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( ( S ` Y ) ` X ) = ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) )
66 65 fveq2d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) )
67 64 fveq2d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( S ` X ) = ( S ` ( ( k .x. E ) .+ u ) ) )
68 67 62 fveq12d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( ( S ` X ) ` Y ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) )
69 61 66 68 3eqtr4d 
 |-  ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )
70 69 3exp 
 |-  ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) -> ( ( v e. ( O ` { E } ) /\ l e. B ) -> ( Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) )
71 70 rexlimdvv 
 |-  ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) -> ( E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) )
72 71 3exp 
 |-  ( ph -> ( ( u e. ( O ` { E } ) /\ k e. B ) -> ( X = ( ( k .x. E ) .+ u ) -> ( E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) ) )
73 72 rexlimdvv 
 |-  ( ph -> ( E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) -> ( E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) )
74 20 21 73 mp2d 
 |-  ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )