Metamath Proof Explorer


Theorem hgmapfval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

Ref Expression
Hypotheses hgmapval.h H = LHyp K
hgmapfval.u U = DVecH K W
hgmapfval.v V = Base U
hgmapfval.t · ˙ = U
hgmapfval.r R = Scalar U
hgmapfval.b B = Base R
hgmapfval.c C = LCDual K W
hgmapfval.s ˙ = C
hgmapfval.m M = HDMap K W
hgmapfval.i I = HGMap K W
hgmapfval.k φ K Y W H
Assertion hgmapfval φ I = x B ι y B | v V M x · ˙ v = y ˙ M v

Proof

Step Hyp Ref Expression
1 hgmapval.h H = LHyp K
2 hgmapfval.u U = DVecH K W
3 hgmapfval.v V = Base U
4 hgmapfval.t · ˙ = U
5 hgmapfval.r R = Scalar U
6 hgmapfval.b B = Base R
7 hgmapfval.c C = LCDual K W
8 hgmapfval.s ˙ = C
9 hgmapfval.m M = HDMap K W
10 hgmapfval.i I = HGMap K W
11 hgmapfval.k φ K Y W H
12 1 hgmapffval K Y HGMap K = w H a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v
13 12 fveq1d K Y HGMap K W = w H a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v W
14 10 13 syl5eq K Y I = w H a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v W
15 fveq2 w = W DVecH K w = DVecH K W
16 15 2 eqtr4di w = W DVecH K w = U
17 fveq2 w = W HDMap K w = HDMap K W
18 17 9 eqtr4di w = W HDMap K w = M
19 2fveq3 w = W LCDual K w = LCDual K W
20 19 oveqd w = W y LCDual K w m v = y LCDual K W m v
21 20 eqeq2d w = W m x u v = y LCDual K w m v m x u v = y LCDual K W m v
22 21 ralbidv w = W v Base u m x u v = y LCDual K w m v v Base u m x u v = y LCDual K W m v
23 22 riotabidv w = W ι y b | v Base u m x u v = y LCDual K w m v = ι y b | v Base u m x u v = y LCDual K W m v
24 23 mpteq2dv w = W x b ι y b | v Base u m x u v = y LCDual K w m v = x b ι y b | v Base u m x u v = y LCDual K W m v
25 24 eleq2d w = W a x b ι y b | v Base u m x u v = y LCDual K w m v a x b ι y b | v Base u m x u v = y LCDual K W m v
26 18 25 sbceqbid w = W [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v [˙M / m]˙ a x b ι y b | v Base u m x u v = y LCDual K W m v
27 26 sbcbidv w = W [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v [˙Base Scalar u / b]˙ [˙M / m]˙ a x b ι y b | v Base u m x u v = y LCDual K W m v
28 16 27 sbceqbid w = W [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v [˙U / u]˙ [˙Base Scalar u / b]˙ [˙M / m]˙ a x b ι y b | v Base u m x u v = y LCDual K W m v
29 2 fvexi U V
30 fvex Base Scalar u V
31 9 fvexi M V
32 simp2 u = U b = Base Scalar u m = M b = Base Scalar u
33 simp1 u = U b = Base Scalar u m = M u = U
34 33 fveq2d u = U b = Base Scalar u m = M Scalar u = Scalar U
35 34 5 eqtr4di u = U b = Base Scalar u m = M Scalar u = R
36 35 fveq2d u = U b = Base Scalar u m = M Base Scalar u = Base R
37 32 36 eqtrd u = U b = Base Scalar u m = M b = Base R
38 37 6 eqtr4di u = U b = Base Scalar u m = M b = B
39 simp2 u = U b = B m = M b = B
40 simp1 u = U b = B m = M u = U
41 40 fveq2d u = U b = B m = M Base u = Base U
42 41 3 eqtr4di u = U b = B m = M Base u = V
43 simp3 u = U b = B m = M m = M
44 40 fveq2d u = U b = B m = M u = U
45 44 4 eqtr4di u = U b = B m = M u = · ˙
46 45 oveqd u = U b = B m = M x u v = x · ˙ v
47 43 46 fveq12d u = U b = B m = M m x u v = M x · ˙ v
48 eqidd u = U b = B m = M LCDual K W = LCDual K W
49 48 7 eqtr4di u = U b = B m = M LCDual K W = C
50 49 fveq2d u = U b = B m = M LCDual K W = C
51 50 8 eqtr4di u = U b = B m = M LCDual K W = ˙
52 eqidd u = U b = B m = M y = y
53 43 fveq1d u = U b = B m = M m v = M v
54 51 52 53 oveq123d u = U b = B m = M y LCDual K W m v = y ˙ M v
55 47 54 eqeq12d u = U b = B m = M m x u v = y LCDual K W m v M x · ˙ v = y ˙ M v
56 42 55 raleqbidv u = U b = B m = M v Base u m x u v = y LCDual K W m v v V M x · ˙ v = y ˙ M v
57 39 56 riotaeqbidv u = U b = B m = M ι y b | v Base u m x u v = y LCDual K W m v = ι y B | v V M x · ˙ v = y ˙ M v
58 39 57 mpteq12dv u = U b = B m = M x b ι y b | v Base u m x u v = y LCDual K W m v = x B ι y B | v V M x · ˙ v = y ˙ M v
59 58 eleq2d u = U b = B m = M a x b ι y b | v Base u m x u v = y LCDual K W m v a x B ι y B | v V M x · ˙ v = y ˙ M v
60 38 59 syld3an2 u = U b = Base Scalar u m = M a x b ι y b | v Base u m x u v = y LCDual K W m v a x B ι y B | v V M x · ˙ v = y ˙ M v
61 29 30 31 60 sbc3ie [˙U / u]˙ [˙Base Scalar u / b]˙ [˙M / m]˙ a x b ι y b | v Base u m x u v = y LCDual K W m v a x B ι y B | v V M x · ˙ v = y ˙ M v
62 28 61 bitrdi w = W [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v a x B ι y B | v V M x · ˙ v = y ˙ M v
63 62 abbi1dv w = W a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v = x B ι y B | v V M x · ˙ v = y ˙ M v
64 eqid w H a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v = w H a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v
65 63 64 6 mptfvmpt W H w H a | [˙ DVecH K w / u]˙ [˙Base Scalar u / b]˙ [˙ HDMap K w / m]˙ a x b ι y b | v Base u m x u v = y LCDual K w m v W = x B ι y B | v V M x · ˙ v = y ˙ M v
66 14 65 sylan9eq K Y W H I = x B ι y B | v V M x · ˙ v = y ˙ M v
67 11 66 syl φ I = x B ι y B | v V M x · ˙ v = y ˙ M v