Metamath Proof Explorer

Theorem hdmapinvlem3

Description: Line 30 in Baer p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hdmapinvlem3.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapinvlem3.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
hdmapinvlem3.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hdmapinvlem3.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapinvlem3.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapinvlem3.p
hdmapinvlem3.m
hdmapinvlem3.q
hdmapinvlem3.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hdmapinvlem3.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
hdmapinvlem3.t
hdmapinvlem3.z
hdmapinvlem3.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapinvlem3.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
hdmapinvlem3.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmapinvlem3.c ${⊢}{\phi }\to {C}\in {O}\left(\left\{{E}\right\}\right)$
hdmapinvlem3.d ${⊢}{\phi }\to {D}\in {O}\left(\left\{{E}\right\}\right)$
hdmapinvlem3.i ${⊢}{\phi }\to {I}\in {B}$
hdmapinvlem3.j ${⊢}{\phi }\to {J}\in {B}$
hdmapinvlem3.ij
Assertion hdmapinvlem3

Proof

Step Hyp Ref Expression
1 hdmapinvlem3.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapinvlem3.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
3 hdmapinvlem3.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
4 hdmapinvlem3.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 hdmapinvlem3.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 hdmapinvlem3.p
7 hdmapinvlem3.m
8 hdmapinvlem3.q
9 hdmapinvlem3.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
10 hdmapinvlem3.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
11 hdmapinvlem3.t
12 hdmapinvlem3.z
13 hdmapinvlem3.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
14 hdmapinvlem3.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
15 hdmapinvlem3.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
16 hdmapinvlem3.c ${⊢}{\phi }\to {C}\in {O}\left(\left\{{E}\right\}\right)$
17 hdmapinvlem3.d ${⊢}{\phi }\to {D}\in {O}\left(\left\{{E}\right\}\right)$
18 hdmapinvlem3.i ${⊢}{\phi }\to {I}\in {B}$
19 hdmapinvlem3.j ${⊢}{\phi }\to {J}\in {B}$
20 hdmapinvlem3.ij
21 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
22 eqid ${⊢}{-}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={-}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
23 1 4 15 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
24 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
25 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
26 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
27 1 24 25 4 5 26 2 15 dvheveccl ${⊢}{\phi }\to {E}\in \left({V}\setminus \left\{{0}_{{U}}\right\}\right)$
28 27 eldifad ${⊢}{\phi }\to {E}\in {V}$
29 5 9 8 10 lmodvscl
30 23 19 28 29 syl3anc
31 28 snssd ${⊢}{\phi }\to \left\{{E}\right\}\subseteq {V}$
32 1 4 5 3 dochssv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left\{{E}\right\}\subseteq {V}\right)\to {O}\left(\left\{{E}\right\}\right)\subseteq {V}$
33 15 31 32 syl2anc ${⊢}{\phi }\to {O}\left(\left\{{E}\right\}\right)\subseteq {V}$
34 33 17 sseldd ${⊢}{\phi }\to {D}\in {V}$
35 1 4 5 7 21 22 13 15 30 34 hdmapsub
36 35 fveq1d
37 eqid ${⊢}{-}_{{R}}={-}_{{R}}$
38 eqid ${⊢}{\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
39 1 4 5 21 38 13 15 30 hdmapcl
40 1 4 5 21 38 13 15 34 hdmapcl ${⊢}{\phi }\to {S}\left({D}\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
41 5 9 8 10 lmodvscl
42 23 18 28 41 syl3anc
43 33 16 sseldd ${⊢}{\phi }\to {C}\in {V}$
44 5 6 lmodvacl
45 23 42 43 44 syl3anc
46 1 4 5 9 37 21 38 22 15 39 40 45 lcdvsubval
47 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
48 1 4 5 6 9 47 13 15 42 43 30 hdmaplna1
49 1 4 5 8 9 10 11 13 14 15 42 28 19 hdmapglnm2
50 1 4 5 8 9 10 11 13 15 28 28 18 hdmaplnm1
51 eqid ${⊢}\mathrm{HVMap}\left({K}\right)\left({W}\right)=\mathrm{HVMap}\left({K}\right)\left({W}\right)$
52 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
53 1 2 51 13 15 4 9 52 hdmapevec2 ${⊢}{\phi }\to {S}\left({E}\right)\left({E}\right)={1}_{{R}}$
54 53 oveq2d
55 9 lmodring ${⊢}{U}\in \mathrm{LMod}\to {R}\in \mathrm{Ring}$
56 23 55 syl ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
57 10 11 52 ringridm
58 56 18 57 syl2anc
59 50 54 58 3eqtrd
60 59 oveq1d
61 49 60 eqtrd
62 1 4 5 8 9 10 11 13 14 15 43 28 19 hdmapglnm2
63 1 2 3 4 5 9 10 11 12 13 15 16 hdmapinvlem1
64 63 oveq1d
65 1 4 9 10 14 15 19 hgmapcl ${⊢}{\phi }\to {G}\left({J}\right)\in {B}$
66 10 11 12 ringlz
67 56 65 66 syl2anc
68 62 64 67 3eqtrd
69 61 68 oveq12d
70 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
71 56 70 syl ${⊢}{\phi }\to {R}\in \mathrm{Grp}$
72 9 10 11 lmodmcl
73 23 18 65 72 syl3anc
74 10 47 12 grprid
75 71 73 74 syl2anc
76 48 69 75 3eqtrd
77 1 4 5 6 9 47 13 15 42 43 34 hdmaplna1
78 1 4 5 8 9 10 11 13 15 28 34 18 hdmaplnm1
79 1 2 3 4 5 9 10 11 12 13 15 17 hdmapinvlem2
80 79 oveq2d
81 10 11 12 ringrz
82 56 18 81 syl2anc
83 78 80 82 3eqtrrd
84 83 20 oveq12d
85 10 47 12 grplid
86 71 73 85 syl2anc
87 77 84 86 3eqtr2d
88 76 87 oveq12d
89 46 88 eqtrd
90 10 12 37 grpsubid
91 71 73 90 syl2anc
92 36 89 91 3eqtrd