# Metamath Proof Explorer

## Theorem mapd0

Description: Projectivity map of the zero subspace. Part of property (f) in Baer p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses mapd0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapd0.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapd0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapd0.o ${⊢}{O}={0}_{{U}}$
mapd0.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapd0.z
mapd0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion mapd0

### Proof

Step Hyp Ref Expression
1 mapd0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapd0.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapd0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapd0.o ${⊢}{O}={0}_{{U}}$
5 mapd0.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 mapd0.z
7 mapd0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
9 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
10 eqid ${⊢}\mathrm{LKer}\left({U}\right)=\mathrm{LKer}\left({U}\right)$
11 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
12 1 3 7 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
13 4 8 lsssn0 ${⊢}{U}\in \mathrm{LMod}\to \left\{{O}\right\}\in \mathrm{LSubSp}\left({U}\right)$
14 12 13 syl ${⊢}{\phi }\to \left\{{O}\right\}\in \mathrm{LSubSp}\left({U}\right)$
15 1 3 8 9 10 11 2 7 14 mapdval ${⊢}{\phi }\to {M}\left(\left\{{O}\right\}\right)=\left\{{f}\in \mathrm{LFnl}\left({U}\right)|\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\subseteq \left\{{O}\right\}\right)\right\}$
16 simprrr ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}$
17 12 adantr ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to {U}\in \mathrm{LMod}$
18 7 adantr ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
19 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
20 simprl ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to {g}\in \mathrm{LFnl}\left({U}\right)$
21 19 9 10 17 20 lkrssv ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{LKer}\left({U}\right)\left({g}\right)\subseteq {\mathrm{Base}}_{{U}}$
22 1 3 19 8 11 dochlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{LKer}\left({U}\right)\left({g}\right)\subseteq {\mathrm{Base}}_{{U}}\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\in \mathrm{LSubSp}\left({U}\right)$
23 18 21 22 syl2anc ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\in \mathrm{LSubSp}\left({U}\right)$
24 4 8 lssle0 ${⊢}\left({U}\in \mathrm{LMod}\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\in \mathrm{LSubSp}\left({U}\right)\right)\to \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}↔\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)=\left\{{O}\right\}\right)$
25 17 23 24 syl2anc ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}↔\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)=\left\{{O}\right\}\right)$
26 16 25 mpbid ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)=\left\{{O}\right\}$
27 26 fveq2d ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{O}\right\}\right)$
28 simprrl ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)$
29 1 3 11 19 4 doch0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{O}\right\}\right)={\mathrm{Base}}_{{U}}$
30 7 29 syl ${⊢}{\phi }\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{O}\right\}\right)={\mathrm{Base}}_{{U}}$
31 30 adantr ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{O}\right\}\right)={\mathrm{Base}}_{{U}}$
32 27 28 31 3eqtr3d ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \mathrm{LKer}\left({U}\right)\left({g}\right)={\mathrm{Base}}_{{U}}$
33 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
34 eqid ${⊢}{0}_{\mathrm{Scalar}\left({U}\right)}={0}_{\mathrm{Scalar}\left({U}\right)}$
35 33 34 19 9 10 lkr0f ${⊢}\left({U}\in \mathrm{LMod}\wedge {g}\in \mathrm{LFnl}\left({U}\right)\right)\to \left(\mathrm{LKer}\left({U}\right)\left({g}\right)={\mathrm{Base}}_{{U}}↔{g}={\mathrm{Base}}_{{U}}×\left\{{0}_{\mathrm{Scalar}\left({U}\right)}\right\}\right)$
36 17 20 35 syl2anc ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to \left(\mathrm{LKer}\left({U}\right)\left({g}\right)={\mathrm{Base}}_{{U}}↔{g}={\mathrm{Base}}_{{U}}×\left\{{0}_{\mathrm{Scalar}\left({U}\right)}\right\}\right)$
37 32 36 mpbid ${⊢}\left({\phi }\wedge \left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)\right)\to {g}={\mathrm{Base}}_{{U}}×\left\{{0}_{\mathrm{Scalar}\left({U}\right)}\right\}$
38 1 3 19 33 34 5 6 7 lcd0v
40 37 39 eqtr4d
41 40 ex
42 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
43 1 5 42 6 7 lcd0vcl
44 1 5 42 3 9 7 43 lcdvbaselfl
45 33 34 19 9 10 lkr0f
46 12 44 45 syl2anc
47 38 46 mpbird
48 47 fveq2d
49 48 fveq2d
50 1 3 11 19 7 dochoc1 ${⊢}{\phi }\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left({\mathrm{Base}}_{{U}}\right)\right)={\mathrm{Base}}_{{U}}$
51 49 50 eqtrd
52 51 47 eqtr4d
53 1 3 11 19 4 doch1 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({\mathrm{Base}}_{{U}}\right)=\left\{{O}\right\}$
54 7 53 syl ${⊢}{\phi }\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({\mathrm{Base}}_{{U}}\right)=\left\{{O}\right\}$
55 48 54 eqtrd
56 eqimss
57 55 56 syl
58 44 52 57 jca32
59 eleq1
60 2fveq3
61 60 fveq2d
62 fveq2
63 61 62 eqeq12d
64 60 sseq1d
65 63 64 anbi12d
66 59 65 anbi12d
67 58 66 syl5ibrcom
68 41 67 impbid
69 2fveq3 ${⊢}{f}={g}\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)$
70 69 fveq2d ${⊢}{f}={g}\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)$
71 fveq2 ${⊢}{f}={g}\to \mathrm{LKer}\left({U}\right)\left({f}\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)$
72 70 71 eqeq12d ${⊢}{f}={g}\to \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)↔\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right)$
73 69 sseq1d ${⊢}{f}={g}\to \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\subseteq \left\{{O}\right\}↔\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)$
74 72 73 anbi12d ${⊢}{f}={g}\to \left(\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\subseteq \left\{{O}\right\}\right)↔\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)$
75 74 elrab ${⊢}{g}\in \left\{{f}\in \mathrm{LFnl}\left({U}\right)|\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({f}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({f}\right)\right)\subseteq \left\{{O}\right\}\right)\right\}↔\left({g}\in \mathrm{LFnl}\left({U}\right)\wedge \left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\wedge \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\subseteq \left\{{O}\right\}\right)\right)$
76 velsn
77 68 75 76 3bitr4g
78 77 eqrdv
79 15 78 eqtrd