Metamath Proof Explorer

Theorem mapdpglem3

Description: Lemma for mapdpg . Baer p. 45, line 3: "infer...the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d g w z ph locally to avoid clashes with later substitutions into ph .) (Contributed by NM, 18-Mar-2015)

Ref Expression
Hypotheses mapdpglem.h 
|- H = ( LHyp ` K )
mapdpglem.m 
|- M = ( ( mapd ` K ) ` W )
mapdpglem.u 
|- U = ( ( DVecH ` K ) ` W )
mapdpglem.v 
|- V = ( Base ` U )
mapdpglem.s 
|- .- = ( -g ` U )
mapdpglem.n 
|- N = ( LSpan ` U )
mapdpglem.c 
|- C = ( ( LCDual ` K ) ` W )
mapdpglem.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdpglem.x 
|- ( ph -> X e. V )
mapdpglem.y 
|- ( ph -> Y e. V )
mapdpglem1.p 
|- .(+) = ( LSSum ` C )
mapdpglem2.j 
|- J = ( LSpan ` C )
mapdpglem3.f 
|- F = ( Base ` C )
mapdpglem3.te 
|- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
mapdpglem3.a 
|- A = ( Scalar ` U )
mapdpglem3.b 
|- B = ( Base ` A )
mapdpglem3.t 
|- .x. = ( .s ` C )
mapdpglem3.r 
|- R = ( -g ` C )
mapdpglem3.g 
|- ( ph -> G e. F )
mapdpglem3.e 
|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
Assertion mapdpglem3 
|- ( ph -> E. g e. B E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) )

Proof

Step Hyp Ref Expression
1 mapdpglem.h 
 |-  H = ( LHyp ` K )
2 mapdpglem.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapdpglem.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 mapdpglem.v 
 |-  V = ( Base ` U )
5 mapdpglem.s 
 |-  .- = ( -g ` U )
6 mapdpglem.n 
 |-  N = ( LSpan ` U )
7 mapdpglem.c 
 |-  C = ( ( LCDual ` K ) ` W )
8 mapdpglem.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 mapdpglem.x 
 |-  ( ph -> X e. V )
10 mapdpglem.y 
 |-  ( ph -> Y e. V )
11 mapdpglem1.p 
 |-  .(+) = ( LSSum ` C )
12 mapdpglem2.j 
 |-  J = ( LSpan ` C )
13 mapdpglem3.f 
 |-  F = ( Base ` C )
14 mapdpglem3.te 
 |-  ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) )
15 mapdpglem3.a 
 |-  A = ( Scalar ` U )
16 mapdpglem3.b 
 |-  B = ( Base ` A )
17 mapdpglem3.t 
 |-  .x. = ( .s ` C )
18 mapdpglem3.r 
 |-  R = ( -g ` C )
19 mapdpglem3.g 
 |-  ( ph -> G e. F )
20 mapdpglem3.e 
 |-  ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )
21 20 oveq1d 
 |-  ( ph -> ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) = ( ( J ` { G } ) .(+) ( M ` ( N ` { Y } ) ) ) )
22 14 21 eleqtrd 
 |-  ( ph -> t e. ( ( J ` { G } ) .(+) ( M ` ( N ` { Y } ) ) ) )
23 r19.41v 
 |-  ( E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> ( E. g e. B w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
24 1 7 8 lcdlmod 
 |-  ( ph -> C e. LMod )
25 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
26 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
27 25 26 13 17 12 lspsnel 
 |-  ( ( C e. LMod /\ G e. F ) -> ( w e. ( J ` { G } ) <-> E. g e. ( Base ` ( Scalar ` C ) ) w = ( g .x. G ) ) )
28 24 19 27 syl2anc 
 |-  ( ph -> ( w e. ( J ` { G } ) <-> E. g e. ( Base ` ( Scalar ` C ) ) w = ( g .x. G ) ) )
29 1 3 15 16 7 25 26 8 lcdsbase 
 |-  ( ph -> ( Base ` ( Scalar ` C ) ) = B )
30 29 rexeqdv 
 |-  ( ph -> ( E. g e. ( Base ` ( Scalar ` C ) ) w = ( g .x. G ) <-> E. g e. B w = ( g .x. G ) ) )
31 28 30 bitrd 
 |-  ( ph -> ( w e. ( J ` { G } ) <-> E. g e. B w = ( g .x. G ) ) )
32 31 anbi1d 
 |-  ( ph -> ( ( w e. ( J ` { G } ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> ( E. g e. B w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) ) )
33 23 32 bitr4id 
 |-  ( ph -> ( E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> ( w e. ( J ` { G } ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) ) )
34 33 exbidv 
 |-  ( ph -> ( E. w E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> E. w ( w e. ( J ` { G } ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) ) )
35 df-rex 
 |-  ( E. w e. ( J ` { G } ) E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) <-> E. w ( w e. ( J ` { G } ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
36 34 35 bitr4di 
 |-  ( ph -> ( E. w E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> E. w e. ( J ` { G } ) E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
37 eqid 
 |-  ( LSubSp ` C ) = ( LSubSp ` C )
38 37 lsssssubg 
 |-  ( C e. LMod -> ( LSubSp ` C ) C_ ( SubGrp ` C ) )
39 24 38 syl 
 |-  ( ph -> ( LSubSp ` C ) C_ ( SubGrp ` C ) )
40 13 37 12 lspsncl 
 |-  ( ( C e. LMod /\ G e. F ) -> ( J ` { G } ) e. ( LSubSp ` C ) )
41 24 19 40 syl2anc 
 |-  ( ph -> ( J ` { G } ) e. ( LSubSp ` C ) )
42 39 41 sseldd 
 |-  ( ph -> ( J ` { G } ) e. ( SubGrp ` C ) )
43 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
44 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
45 4 43 6 lspsncl 
 |-  ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )
46 44 10 45 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )
47 1 2 3 43 7 37 8 46 mapdcl2 
 |-  ( ph -> ( M ` ( N ` { Y } ) ) e. ( LSubSp ` C ) )
48 39 47 sseldd 
 |-  ( ph -> ( M ` ( N ` { Y } ) ) e. ( SubGrp ` C ) )
49 18 11 42 48 lsmelvalm 
 |-  ( ph -> ( t e. ( ( J ` { G } ) .(+) ( M ` ( N ` { Y } ) ) ) <-> E. w e. ( J ` { G } ) E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
50 36 49 bitr4d 
 |-  ( ph -> ( E. w E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> t e. ( ( J ` { G } ) .(+) ( M ` ( N ` { Y } ) ) ) ) )
51 22 50 mpbird 
 |-  ( ph -> E. w E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
52 ovex 
 |-  ( g .x. G ) e. _V
53 oveq1 
 |-  ( w = ( g .x. G ) -> ( w R z ) = ( ( g .x. G ) R z ) )
54 53 eqeq2d 
 |-  ( w = ( g .x. G ) -> ( t = ( w R z ) <-> t = ( ( g .x. G ) R z ) ) )
55 54 rexbidv 
 |-  ( w = ( g .x. G ) -> ( E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) <-> E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) ) )
56 52 55 ceqsexv 
 |-  ( E. w ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) )
57 56 rexbii 
 |-  ( E. g e. B E. w ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> E. g e. B E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) )
58 rexcom4 
 |-  ( E. g e. B E. w ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) <-> E. w E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
59 57 58 bitr3i 
 |-  ( E. g e. B E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) <-> E. w E. g e. B ( w = ( g .x. G ) /\ E. z e. ( M ` ( N ` { Y } ) ) t = ( w R z ) ) )
60 51 59 sylibr 
 |-  ( ph -> E. g e. B E. z e. ( M ` ( N ` { Y } ) ) t = ( ( g .x. G ) R z ) )