Metamath Proof Explorer


Theorem hgmapvvlem2

Description: Lemma for hgmapvv . Eliminate Y (Baer's s). (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hdmapglem6.h H = LHyp K
hdmapglem6.e E = I Base K I LTrn K W
hdmapglem6.o O = ocH K W
hdmapglem6.u U = DVecH K W
hdmapglem6.v V = Base U
hdmapglem6.q · ˙ = U
hdmapglem6.r R = Scalar U
hdmapglem6.b B = Base R
hdmapglem6.t × ˙ = R
hdmapglem6.z 0 ˙ = 0 R
hdmapglem6.i 1 ˙ = 1 R
hdmapglem6.n N = inv r R
hdmapglem6.s S = HDMap K W
hdmapglem6.g G = HGMap K W
hdmapglem6.k φ K HL W H
hdmapglem6.x φ X B 0 ˙
hdmapglem6.c φ C O E
hdmapglem6.d φ D O E
hdmapglem6.cd φ S D C = 1 ˙
Assertion hgmapvvlem2 φ G G X = X

Proof

Step Hyp Ref Expression
1 hdmapglem6.h H = LHyp K
2 hdmapglem6.e E = I Base K I LTrn K W
3 hdmapglem6.o O = ocH K W
4 hdmapglem6.u U = DVecH K W
5 hdmapglem6.v V = Base U
6 hdmapglem6.q · ˙ = U
7 hdmapglem6.r R = Scalar U
8 hdmapglem6.b B = Base R
9 hdmapglem6.t × ˙ = R
10 hdmapglem6.z 0 ˙ = 0 R
11 hdmapglem6.i 1 ˙ = 1 R
12 hdmapglem6.n N = inv r R
13 hdmapglem6.s S = HDMap K W
14 hdmapglem6.g G = HGMap K W
15 hdmapglem6.k φ K HL W H
16 hdmapglem6.x φ X B 0 ˙
17 hdmapglem6.c φ C O E
18 hdmapglem6.d φ D O E
19 hdmapglem6.cd φ S D C = 1 ˙
20 1 4 15 dvhlvec φ U LVec
21 7 lvecdrng U LVec R DivRing
22 20 21 syl φ R DivRing
23 16 eldifad φ X B
24 1 4 7 8 14 15 23 hgmapcl φ G X B
25 eldifsni X B 0 ˙ X 0 ˙
26 16 25 syl φ X 0 ˙
27 1 4 7 8 10 14 15 23 hgmapeq0 φ G X = 0 ˙ X = 0 ˙
28 27 necon3bid φ G X 0 ˙ X 0 ˙
29 26 28 mpbird φ G X 0 ˙
30 8 10 12 drnginvrcl R DivRing G X B G X 0 ˙ N G X B
31 22 24 29 30 syl3anc φ N G X B
32 8 10 12 drnginvrn0 R DivRing G X B G X 0 ˙ N G X 0 ˙
33 22 24 29 32 syl3anc φ N G X 0 ˙
34 eldifsn N G X B 0 ˙ N G X B N G X 0 ˙
35 31 33 34 sylanbrc φ N G X B 0 ˙
36 8 10 9 11 12 drnginvrl R DivRing G X B G X 0 ˙ N G X × ˙ G X = 1 ˙
37 22 24 29 36 syl3anc φ N G X × ˙ G X = 1 ˙
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 35 37 hgmapvvlem1 φ G G X = X