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=LHyp⁡K
mapd0.m ⊢M=mapd⁡K⁡W
mapd0.u ⊢U=DVecH⁡K⁡W
mapd0.o ⊢O=0U
mapd0.c ⊢C=LCDual⁡K⁡W
mapd0.z ⊢0˙=0C
mapd0.k ⊢φ→K∈HL∧W∈H
Assertion mapd0 ⊢φ→M⁡O=0˙

Proof

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