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 = 0 U
mapd0.c ⊢ C = LCDual ⁡ K ⁡ W
mapd0.z ⊢ 0 ˙ = 0 C
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 = 0 U
5 mapd0.c ⊢ C = LCDual ⁡ K ⁡ W
6 mapd0.z ⊢ 0 ˙ = 0 C
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 ⊢ Base U = Base U
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 ⊆ Base U
22 1 3 19 8 11 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ LKer ⁡ U ⁡ g ⊆ Base U → 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 = Base U
30 7 29 syl ⊢ φ → ocH ⁡ K ⁡ W ⁡ O = Base U
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 = Base U
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 = Base U
33 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
34 eqid ⊢ 0 Scalar ⁡ U = 0 Scalar ⁡ U
35 33 34 19 9 10 lkr0f ⊢ U ∈ LMod ∧ g ∈ LFnl ⁡ U → LKer ⁡ U ⁡ g = Base U ↔ g = Base U × 0 Scalar ⁡ 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 = Base U ↔ g = Base U × 0 Scalar ⁡ 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 = Base U × 0 Scalar ⁡ U
38 1 3 19 33 34 5 6 7 lcd0v ⊢ φ → 0 ˙ = Base U × 0 Scalar ⁡ 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 ˙ = Base U × 0 Scalar ⁡ 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 ⊢ Base C = Base C
43 1 5 42 6 7 lcd0vcl ⊢ φ → 0 ˙ ∈ Base C
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 ˙ = Base U ↔ 0 ˙ = Base U × 0 Scalar ⁡ U
46 12 44 45 syl2anc ⊢ φ → LKer ⁡ U ⁡ 0 ˙ = Base U ↔ 0 ˙ = Base U × 0 Scalar ⁡ U
47 38 46 mpbird ⊢ φ → LKer ⁡ U ⁡ 0 ˙ = Base U
48 47 fveq2d ⊢ φ → ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ 0 ˙ = ocH ⁡ K ⁡ W ⁡ Base U
49 48 fveq2d ⊢ φ → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ 0 ˙ = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ Base U
50 1 3 11 19 7 dochoc1 ⊢ φ → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ Base U = Base U
51 49 50 eqtrd ⊢ φ → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ 0 ˙ = Base U
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 ⁡ Base U = O
54 7 53 syl ⊢ φ → ocH ⁡ K ⁡ W ⁡ Base U = 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 ˙