# Metamath Proof Explorer

## Theorem mapdpglem30

Description: Lemma for mapdpg . Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 , using lvecindp2 ) that v = 1 and v = u...". TODO: would it be shorter to have only the v = ( 1rA ) part and use mapdpglem28.u2 in mapdpglem31 ? (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses mapdpg.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdpg.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdpg.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdpg.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdpg.s
mapdpg.z
mapdpg.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdpg.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdpg.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
mapdpg.r ${⊢}{R}={-}_{{C}}$
mapdpg.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdpg.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdpg.x
mapdpg.y
mapdpg.g ${⊢}{\phi }\to {G}\in {F}$
mapdpg.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
mapdpg.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
mapdpgem25.h1
mapdpgem25.i1
mapdpglem26.a ${⊢}{A}=\mathrm{Scalar}\left({U}\right)$
mapdpglem26.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mapdpglem26.t
mapdpglem26.o ${⊢}{O}={0}_{{A}}$
mapdpglem28.ve ${⊢}{\phi }\to {v}\in {B}$
mapdpglem28.u1
mapdpglem28.u2
mapdpglem28.ue ${⊢}{\phi }\to {u}\in {B}$
Assertion mapdpglem30 ${⊢}{\phi }\to \left({v}={1}_{{A}}\wedge {v}={u}\right)$

### Proof

Step Hyp Ref Expression
1 mapdpg.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdpg.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdpg.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdpg.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 mapdpg.s
6 mapdpg.z
7 mapdpg.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 mapdpg.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
9 mapdpg.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
10 mapdpg.r ${⊢}{R}={-}_{{C}}$
11 mapdpg.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 mapdpg.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
13 mapdpg.x
14 mapdpg.y
15 mapdpg.g ${⊢}{\phi }\to {G}\in {F}$
16 mapdpg.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
17 mapdpg.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
18 mapdpgem25.h1
19 mapdpgem25.i1
20 mapdpglem26.a ${⊢}{A}=\mathrm{Scalar}\left({U}\right)$
21 mapdpglem26.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
22 mapdpglem26.t
23 mapdpglem26.o ${⊢}{O}={0}_{{A}}$
24 mapdpglem28.ve ${⊢}{\phi }\to {v}\in {B}$
25 mapdpglem28.u1
26 mapdpglem28.u2
27 mapdpglem28.ue ${⊢}{\phi }\to {u}\in {B}$
28 eqid ${⊢}{+}_{{C}}={+}_{{C}}$
29 eqid ${⊢}\mathrm{Scalar}\left({C}\right)=\mathrm{Scalar}\left({C}\right)$
30 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
31 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
32 1 8 12 lcdlvec ${⊢}{\phi }\to {C}\in \mathrm{LVec}$
33 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 mapdpglem30a ${⊢}{\phi }\to {G}\ne {0}_{{C}}$
34 eldifsn ${⊢}{G}\in \left({F}\setminus \left\{{0}_{{C}}\right\}\right)↔\left({G}\in {F}\wedge {G}\ne {0}_{{C}}\right)$
35 15 33 34 sylanbrc ${⊢}{\phi }\to {G}\in \left({F}\setminus \left\{{0}_{{C}}\right\}\right)$
36 19 simpld ${⊢}{\phi }\to {i}\in {F}$
37 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 mapdpglem30b ${⊢}{\phi }\to {i}\ne {0}_{{C}}$
38 eldifsn ${⊢}{i}\in \left({F}\setminus \left\{{0}_{{C}}\right\}\right)↔\left({i}\in {F}\wedge {i}\ne {0}_{{C}}\right)$
39 36 37 38 sylanbrc ${⊢}{\phi }\to {i}\in \left({F}\setminus \left\{{0}_{{C}}\right\}\right)$
40 1 3 20 21 8 29 30 12 lcdsbase ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}={B}$
41 24 40 eleqtrrd ${⊢}{\phi }\to {v}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
42 1 3 12 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
43 20 lmodring ${⊢}{U}\in \mathrm{LMod}\to {A}\in \mathrm{Ring}$
44 42 43 syl ${⊢}{\phi }\to {A}\in \mathrm{Ring}$
45 ringgrp ${⊢}{A}\in \mathrm{Ring}\to {A}\in \mathrm{Grp}$
46 44 45 syl ${⊢}{\phi }\to {A}\in \mathrm{Grp}$
47 eqid ${⊢}{1}_{{A}}={1}_{{A}}$
48 21 47 ringidcl ${⊢}{A}\in \mathrm{Ring}\to {1}_{{A}}\in {B}$
49 44 48 syl ${⊢}{\phi }\to {1}_{{A}}\in {B}$
50 eqid ${⊢}{inv}_{g}\left({A}\right)={inv}_{g}\left({A}\right)$
51 21 50 grpinvcl ${⊢}\left({A}\in \mathrm{Grp}\wedge {1}_{{A}}\in {B}\right)\to {inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}$
52 46 49 51 syl2anc ${⊢}{\phi }\to {inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}$
53 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
54 21 53 ringcl ${⊢}\left({A}\in \mathrm{Ring}\wedge {v}\in {B}\wedge {inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}\right)\to {v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}$
55 44 24 52 54 syl3anc ${⊢}{\phi }\to {v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}$
56 55 40 eleqtrrd ${⊢}{\phi }\to {v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
57 49 40 eleqtrrd ${⊢}{\phi }\to {1}_{{A}}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
58 21 53 ringcl ${⊢}\left({A}\in \mathrm{Ring}\wedge {u}\in {B}\wedge {inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}\right)\to {u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}$
59 44 27 52 58 syl3anc ${⊢}{\phi }\to {u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {B}$
60 59 40 eleqtrrd ${⊢}{\phi }\to {u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
61 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 mapdpglem29 ${⊢}{\phi }\to {J}\left(\left\{{G}\right\}\right)\ne {J}\left(\left\{{i}\right\}\right)$
62 1 3 20 21 53 8 9 22 12 52 27 36 lcdvsass
63 62 oveq2d
64 1 3 20 21 8 9 22 12 49 15 lcdvscl
65 1 3 20 21 8 9 22 12 27 36 lcdvscl
66 1 3 20 50 47 8 9 28 22 10 12 64 65 lcdvsub
67 1 3 20 21 53 8 9 22 12 52 24 36 lcdvsass
68 67 oveq2d
69 1 3 20 21 8 9 22 12 24 15 lcdvscl
70 1 3 20 21 8 9 22 12 24 36 lcdvscl
71 1 3 20 50 47 8 9 28 22 10 12 69 70 lcdvsub
72 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 mapdpglem28
73 eqid ${⊢}{1}_{\mathrm{Scalar}\left({C}\right)}={1}_{\mathrm{Scalar}\left({C}\right)}$
74 1 3 20 47 8 29 73 12 lcd1 ${⊢}{\phi }\to {1}_{\mathrm{Scalar}\left({C}\right)}={1}_{{A}}$
75 74 oveq1d
76 1 8 12 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
77 9 29 22 73 lmodvs1
78 76 15 77 syl2anc
79 75 78 eqtr3d
80 79 oveq1d
81 72 80 eqtr4d
82 68 71 81 3eqtr2rd
83 63 66 82 3eqtr2rd
84 9 28 29 30 22 31 11 32 35 39 41 56 57 60 61 83 lvecindp2 ${⊢}{\phi }\to \left({v}={1}_{{A}}\wedge {v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)={u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\right)$
85 21 53 47 50 44 24 rngnegr ${⊢}{\phi }\to {v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)={inv}_{g}\left({A}\right)\left({v}\right)$
86 21 53 47 50 44 27 rngnegr ${⊢}{\phi }\to {u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)={inv}_{g}\left({A}\right)\left({u}\right)$
87 85 86 eqeq12d ${⊢}{\phi }\to \left({v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)={u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)↔{inv}_{g}\left({A}\right)\left({v}\right)={inv}_{g}\left({A}\right)\left({u}\right)\right)$
88 21 50 46 24 27 grpinv11 ${⊢}{\phi }\to \left({inv}_{g}\left({A}\right)\left({v}\right)={inv}_{g}\left({A}\right)\left({u}\right)↔{v}={u}\right)$
89 87 88 bitrd ${⊢}{\phi }\to \left({v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)={u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)↔{v}={u}\right)$
90 89 anbi2d ${⊢}{\phi }\to \left(\left({v}={1}_{{A}}\wedge {v}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)={u}{\cdot }_{{A}}{inv}_{g}\left({A}\right)\left({1}_{{A}}\right)\right)↔\left({v}={1}_{{A}}\wedge {v}={u}\right)\right)$
91 84 90 mpbid ${⊢}{\phi }\to \left({v}={1}_{{A}}\wedge {v}={u}\right)$