Metamath Proof Explorer


Theorem mapdrvallem2

Description: Lemma for mapdrval . TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015)

Ref Expression
Hypotheses mapdrval.h H = LHyp K
mapdrval.o O = ocH K W
mapdrval.m M = mapd K W
mapdrval.u U = DVecH K W
mapdrval.s S = LSubSp U
mapdrval.f F = LFnl U
mapdrval.l L = LKer U
mapdrval.d D = LDual U
mapdrval.t T = LSubSp D
mapdrval.c C = g F | O O L g = L g
mapdrval.k φ K HL W H
mapdrval.r φ R T
mapdrval.e φ R C
mapdrval.q Q = h R O L h
mapdrval.v V = Base U
mapdrvallem2.a A = LSAtoms U
mapdrvallem2.n N = LSpan U
mapdrvallem2.z 0 ˙ = 0 U
mapdrvallem2.y Y = 0 D
Assertion mapdrvallem2 φ f C | O L f Q R

Proof

Step Hyp Ref Expression
1 mapdrval.h H = LHyp K
2 mapdrval.o O = ocH K W
3 mapdrval.m M = mapd K W
4 mapdrval.u U = DVecH K W
5 mapdrval.s S = LSubSp U
6 mapdrval.f F = LFnl U
7 mapdrval.l L = LKer U
8 mapdrval.d D = LDual U
9 mapdrval.t T = LSubSp D
10 mapdrval.c C = g F | O O L g = L g
11 mapdrval.k φ K HL W H
12 mapdrval.r φ R T
13 mapdrval.e φ R C
14 mapdrval.q Q = h R O L h
15 mapdrval.v V = Base U
16 mapdrvallem2.a A = LSAtoms U
17 mapdrvallem2.n N = LSpan U
18 mapdrvallem2.z 0 ˙ = 0 U
19 mapdrvallem2.y Y = 0 D
20 eleq1 f = Y f R Y R
21 11 3ad2ant1 φ f C O L f Q K HL W H
22 21 adantr φ f C O L f Q f Y K HL W H
23 simpl2 φ f C O L f Q f Y f C
24 simpr φ f C O L f Q f Y f Y
25 eldifsn f C Y f C f Y
26 23 24 25 sylanbrc φ f C O L f Q f Y f C Y
27 1 2 4 15 17 18 6 7 8 19 10 22 26 lcfl8b φ f C O L f Q f Y x V 0 ˙ O L f = N x
28 simp1l3 φ f C O L f Q f Y x V 0 ˙ O L f = N x O L f Q
29 eqimss2 O L f = N x N x O L f
30 29 3ad2ant3 φ f C O L f Q f Y x V 0 ˙ O L f = N x N x O L f
31 1 4 11 dvhlmod φ U LMod
32 31 3ad2ant1 φ f C O L f Q U LMod
33 32 adantr φ f C O L f Q f Y U LMod
34 33 3ad2ant1 φ f C O L f Q f Y x V 0 ˙ O L f = N x U LMod
35 22 3ad2ant1 φ f C O L f Q f Y x V 0 ˙ O L f = N x K HL W H
36 10 lcfl1lem f C f F O O L f = L f
37 36 simplbi f C f F
38 37 3ad2ant2 φ f C O L f Q f F
39 38 adantr φ f C O L f Q f Y f F
40 39 3ad2ant1 φ f C O L f Q f Y x V 0 ˙ O L f = N x f F
41 15 6 7 34 40 lkrssv φ f C O L f Q f Y x V 0 ˙ O L f = N x L f V
42 1 4 15 5 2 dochlss K HL W H L f V O L f S
43 35 41 42 syl2anc φ f C O L f Q f Y x V 0 ˙ O L f = N x O L f S
44 eldifi x V 0 ˙ x V
45 44 3ad2ant2 φ f C O L f Q f Y x V 0 ˙ O L f = N x x V
46 15 5 17 34 43 45 lspsnel5 φ f C O L f Q f Y x V 0 ˙ O L f = N x x O L f N x O L f
47 30 46 mpbird φ f C O L f Q f Y x V 0 ˙ O L f = N x x O L f
48 28 47 sseldd φ f C O L f Q f Y x V 0 ˙ O L f = N x x Q
49 48 14 eleqtrdi φ f C O L f Q f Y x V 0 ˙ O L f = N x x h R O L h
50 eliun x h R O L h h R x O L h
51 49 50 sylib φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h
52 eqid Scalar U = Scalar U
53 eqid Base Scalar U = Base Scalar U
54 eqid D = D
55 1 4 11 dvhlvec φ U LVec
56 55 3ad2ant1 φ f C O L f Q U LVec
57 56 adantr φ f C O L f Q f Y U LVec
58 57 3ad2ant1 φ f C O L f Q f Y x V 0 ˙ O L f = N x U LVec
59 58 ad2antrr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h U LVec
60 simpr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R h R
61 simp1l1 φ f C O L f Q f Y x V 0 ˙ O L f = N x φ
62 61 adantr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R φ
63 62 13 syl φ f C O L f Q f Y x V 0 ˙ O L f = N x h R R C
64 63 sseld φ f C O L f Q f Y x V 0 ˙ O L f = N x h R h R h C
65 10 lcfl1lem h C h F O O L h = L h
66 65 simplbi h C h F
67 64 66 syl6 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R h R h F
68 60 67 mpd φ f C O L f Q f Y x V 0 ˙ O L f = N x h R h F
69 68 adantr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h h F
70 40 ad2antrr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h f F
71 simpll3 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h O L f = N x
72 34 ad2antrr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h U LMod
73 35 ad2antrr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h K HL W H
74 15 6 7 72 69 lkrssv φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h L h V
75 1 4 15 5 2 dochlss K HL W H L h V O L h S
76 73 74 75 syl2anc φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h O L h S
77 simpr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h x O L h
78 5 17 72 76 77 lspsnel5a φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h N x O L h
79 simpll2 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h x V 0 ˙
80 15 17 18 16 72 79 lsatlspsn φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h N x A
81 1 2 4 18 16 6 7 73 69 dochsat0 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h O L h A O L h = 0 ˙
82 18 16 59 80 81 lsatcmp2 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h N x O L h N x = O L h
83 78 82 mpbid φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h N x = O L h
84 71 83 eqtr2d φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h O L h = O L f
85 eqid DIsoH K W = DIsoH K W
86 61 13 syl φ f C O L f Q f Y x V 0 ˙ O L f = N x R C
87 86 sselda φ f C O L f Q f Y x V 0 ˙ O L f = N x h R h C
88 87 adantr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h h C
89 1 85 2 4 6 7 10 73 69 lcfl5 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h h C L h ran DIsoH K W
90 88 89 mpbid φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h L h ran DIsoH K W
91 simp1l2 φ f C O L f Q f Y x V 0 ˙ O L f = N x f C
92 91 ad2antrr φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h f C
93 1 85 2 4 6 7 10 73 70 lcfl5 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h f C L f ran DIsoH K W
94 92 93 mpbid φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h L f ran DIsoH K W
95 1 85 2 73 90 94 doch11 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h O L h = O L f L h = L f
96 84 95 mpbid φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h L h = L f
97 52 53 6 7 8 54 59 69 70 96 eqlkr4 φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h r Base Scalar U f = r D h
98 97 ex φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h r Base Scalar U f = r D h
99 98 reximdva φ f C O L f Q f Y x V 0 ˙ O L f = N x h R x O L h h R r Base Scalar U f = r D h
100 51 99 mpd φ f C O L f Q f Y x V 0 ˙ O L f = N x h R r Base Scalar U f = r D h
101 eleq1 f = r D h f R r D h R
102 101 reximi r Base Scalar U f = r D h r Base Scalar U f R r D h R
103 102 reximi h R r Base Scalar U f = r D h h R r Base Scalar U f R r D h R
104 rexcom h R r Base Scalar U f R r D h R r Base Scalar U h R f R r D h R
105 df-rex h R f R r D h R h h R f R r D h R
106 105 rexbii r Base Scalar U h R f R r D h R r Base Scalar U h h R f R r D h R
107 104 106 bitri h R r Base Scalar U f R r D h R r Base Scalar U h h R f R r D h R
108 103 107 sylib h R r Base Scalar U f = r D h r Base Scalar U h h R f R r D h R
109 100 108 syl φ f C O L f Q f Y x V 0 ˙ O L f = N x r Base Scalar U h h R f R r D h R
110 33 ad2antrr φ f C O L f Q f Y r Base Scalar U h R f R r D h R U LMod
111 12 3ad2ant1 φ f C O L f Q R T
112 111 adantr φ f C O L f Q f Y R T
113 112 ad2antrr φ f C O L f Q f Y r Base Scalar U h R f R r D h R R T
114 simplr φ f C O L f Q f Y r Base Scalar U h R f R r D h R r Base Scalar U
115 simprl φ f C O L f Q f Y r Base Scalar U h R f R r D h R h R
116 52 53 8 54 9 110 113 114 115 ldualssvscl φ f C O L f Q f Y r Base Scalar U h R f R r D h R r D h R
117 biimpr f R r D h R r D h R f R
118 117 ad2antll φ f C O L f Q f Y r Base Scalar U h R f R r D h R r D h R f R
119 116 118 mpd φ f C O L f Q f Y r Base Scalar U h R f R r D h R f R
120 119 ex φ f C O L f Q f Y r Base Scalar U h R f R r D h R f R
121 120 exlimdv φ f C O L f Q f Y r Base Scalar U h h R f R r D h R f R
122 121 rexlimdva φ f C O L f Q f Y r Base Scalar U h h R f R r D h R f R
123 122 3ad2ant1 φ f C O L f Q f Y x V 0 ˙ O L f = N x r Base Scalar U h h R f R r D h R f R
124 109 123 mpd φ f C O L f Q f Y x V 0 ˙ O L f = N x f R
125 124 rexlimdv3a φ f C O L f Q f Y x V 0 ˙ O L f = N x f R
126 27 125 mpd φ f C O L f Q f Y f R
127 8 31 lduallmod φ D LMod
128 127 3ad2ant1 φ f C O L f Q D LMod
129 19 9 lss0cl D LMod R T Y R
130 128 111 129 syl2anc φ f C O L f Q Y R
131 20 126 130 pm2.61ne φ f C O L f Q f R
132 131 rabssdv φ f C | O L f Q R