Metamath Proof Explorer


Theorem dih1dimatlem

Description: Lemma for dih1dimat . (Contributed by NM, 10-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h H = LHyp K
dih1dimat.u U = DVecH K W
dih1dimat.i I = DIsoH K W
dih1dimat.a A = LSAtoms U
dih1dimat.b B = Base K
dih1dimat.l ˙ = K
dih1dimat.c C = Atoms K
dih1dimat.p P = oc K W
dih1dimat.t T = LTrn K W
dih1dimat.r R = trL K W
dih1dimat.e E = TEndo K W
dih1dimat.o O = h T I B
dih1dimat.d F = Scalar U
dih1dimat.j J = inv r F
dih1dimat.v V = Base U
dih1dimat.m · ˙ = U
dih1dimat.s S = LSubSp U
dih1dimat.n N = LSpan U
dih1dimat.z 0 ˙ = 0 U
dih1dimat.g G = ι h T | h P = J s f P
Assertion dih1dimatlem K HL W H D A D ran I

Proof

Step Hyp Ref Expression
1 dih1dimat.h H = LHyp K
2 dih1dimat.u U = DVecH K W
3 dih1dimat.i I = DIsoH K W
4 dih1dimat.a A = LSAtoms U
5 dih1dimat.b B = Base K
6 dih1dimat.l ˙ = K
7 dih1dimat.c C = Atoms K
8 dih1dimat.p P = oc K W
9 dih1dimat.t T = LTrn K W
10 dih1dimat.r R = trL K W
11 dih1dimat.e E = TEndo K W
12 dih1dimat.o O = h T I B
13 dih1dimat.d F = Scalar U
14 dih1dimat.j J = inv r F
15 dih1dimat.v V = Base U
16 dih1dimat.m · ˙ = U
17 dih1dimat.s S = LSubSp U
18 dih1dimat.n N = LSpan U
19 dih1dimat.z 0 ˙ = 0 U
20 dih1dimat.g G = ι h T | h P = J s f P
21 id K HL W H K HL W H
22 1 2 21 dvhlvec K HL W H U LVec
23 15 18 19 4 islsat U LVec D A v V 0 ˙ D = N v
24 22 23 syl K HL W H D A v V 0 ˙ D = N v
25 24 biimpa K HL W H D A v V 0 ˙ D = N v
26 eldifi v V 0 ˙ v V
27 1 9 11 2 15 dvhvbase K HL W H V = T × E
28 27 eleq2d K HL W H v V v T × E
29 26 28 syl5ib K HL W H v V 0 ˙ v T × E
30 29 imp K HL W H v V 0 ˙ v T × E
31 simpr K HL W H f T s E s = O s = O
32 31 opeq2d K HL W H f T s E s = O f s = f O
33 32 sneqd K HL W H f T s E s = O f s = f O
34 33 fveq2d K HL W H f T s E s = O N f s = N f O
35 simpl K HL W H f T K HL W H
36 5 1 9 10 trlcl K HL W H f T R f B
37 6 1 9 10 trlle K HL W H f T R f ˙ W
38 eqid DIsoB K W = DIsoB K W
39 5 6 1 3 38 dihvalb K HL W H R f B R f ˙ W I R f = DIsoB K W R f
40 35 36 37 39 syl12anc K HL W H f T I R f = DIsoB K W R f
41 5 1 9 10 12 2 38 18 dib1dim2 K HL W H f T DIsoB K W R f = N f O
42 40 41 eqtr2d K HL W H f T N f O = I R f
43 5 1 3 2 17 dihf11 K HL W H I : B 1-1 S
44 43 adantr K HL W H f T I : B 1-1 S
45 f1fn I : B 1-1 S I Fn B
46 44 45 syl K HL W H f T I Fn B
47 fnfvelrn I Fn B R f B I R f ran I
48 46 36 47 syl2anc K HL W H f T I R f ran I
49 42 48 eqeltrd K HL W H f T N f O ran I
50 49 adantrr K HL W H f T s E N f O ran I
51 50 adantr K HL W H f T s E s = O N f O ran I
52 34 51 eqeltrd K HL W H f T s E s = O N f s ran I
53 simpll K HL W H f T s E s O K HL W H
54 eqid Base F = Base F
55 1 11 2 13 54 dvhbase K HL W H Base F = E
56 53 55 syl K HL W H f T s E s O Base F = E
57 56 rexeqdv K HL W H f T s E s O t Base F u = t · ˙ f s t E u = t · ˙ f s
58 simplll K HL W H f T s E s O t E K HL W H
59 simpr K HL W H f T s E s O t E t E
60 opelxpi f T s E f s T × E
61 60 ad3antlr K HL W H f T s E s O t E f s T × E
62 1 9 11 2 16 dvhvscacl K HL W H t E f s T × E t · ˙ f s T × E
63 58 59 61 62 syl12anc K HL W H f T s E s O t E t · ˙ f s T × E
64 eleq1a t · ˙ f s T × E u = t · ˙ f s u T × E
65 63 64 syl K HL W H f T s E s O t E u = t · ˙ f s u T × E
66 65 rexlimdva K HL W H f T s E s O t E u = t · ˙ f s u T × E
67 66 pm4.71rd K HL W H f T s E s O t E u = t · ˙ f s u T × E t E u = t · ˙ f s
68 simplrl K HL W H f T s E s O f T
69 68 adantr K HL W H f T s E s O t E f T
70 simplrr K HL W H f T s E s O s E
71 70 adantr K HL W H f T s E s O t E s E
72 1 9 11 2 16 dvhopvsca K HL W H t E f T s E t · ˙ f s = t f t s
73 58 59 69 71 72 syl13anc K HL W H f T s E s O t E t · ˙ f s = t f t s
74 73 eqeq2d K HL W H f T s E s O t E u = t · ˙ f s u = t f t s
75 74 rexbidva K HL W H f T s E s O t E u = t · ˙ f s t E u = t f t s
76 75 anbi2d K HL W H f T s E s O u T × E t E u = t · ˙ f s u T × E t E u = t f t s
77 57 67 76 3bitrd K HL W H f T s E s O t Base F u = t · ˙ f s u T × E t E u = t f t s
78 77 abbidv K HL W H f T s E s O u | t Base F u = t · ˙ f s = u | u T × E t E u = t f t s
79 df-rab u T × E | t E u = t f t s = u | u T × E t E u = t f t s
80 78 79 eqtr4di K HL W H f T s E s O u | t Base F u = t · ˙ f s = u T × E | t E u = t f t s
81 ssrab2 u T × E | t E u = t f t s T × E
82 relxp Rel T × E
83 relss u T × E | t E u = t f t s T × E Rel T × E Rel u T × E | t E u = t f t s
84 81 82 83 mp2 Rel u T × E | t E u = t f t s
85 relopabv Rel g r | g = r G r E
86 vex i V
87 vex p V
88 eqeq1 g = i g = r G i = r G
89 88 anbi1d g = i g = r G r E i = r G r E
90 fveq1 r = p r G = p G
91 90 eqeq2d r = p i = r G i = p G
92 eleq1w r = p r E p E
93 91 92 anbi12d r = p i = r G r E i = p G p E
94 86 87 89 93 opelopab i p g r | g = r G r E i = p G p E
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem0 K HL W H f T s E s O i = p G p E i T p E t E i = t f p = t s
96 95 3expa K HL W H f T s E s O i = p G p E i T p E t E i = t f p = t s
97 opelxp i p T × E i T p E
98 86 87 opth i p = t f t s i = t f p = t s
99 98 rexbii t E i p = t f t s t E i = t f p = t s
100 97 99 anbi12i i p T × E t E i p = t f t s i T p E t E i = t f p = t s
101 96 100 bitr4di K HL W H f T s E s O i = p G p E i p T × E t E i p = t f t s
102 eqeq1 u = i p u = t f t s i p = t f t s
103 102 rexbidv u = i p t E u = t f t s t E i p = t f t s
104 103 elrab i p u T × E | t E u = t f t s i p T × E t E i p = t f t s
105 101 104 bitr4di K HL W H f T s E s O i = p G p E i p u T × E | t E u = t f t s
106 94 105 bitr2id K HL W H f T s E s O i p u T × E | t E u = t f t s i p g r | g = r G r E
107 84 85 106 eqrelrdv K HL W H f T s E s O u T × E | t E u = t f t s = g r | g = r G r E
108 80 107 eqtrd K HL W H f T s E s O u | t Base F u = t · ˙ f s = g r | g = r G r E
109 1 2 53 dvhlmod K HL W H f T s E s O U LMod
110 1 9 11 2 15 dvhelvbasei K HL W H f T s E f s V
111 110 adantr K HL W H f T s E s O f s V
112 13 54 15 16 18 lspsn U LMod f s V N f s = u | t Base F u = t · ˙ f s
113 109 111 112 syl2anc K HL W H f T s E s O N f s = u | t Base F u = t · ˙ f s
114 simpr K HL W H f T s E s O s O
115 5 1 9 11 12 2 13 14 tendoinvcl K HL W H s E s O J s E J s O
116 115 simpld K HL W H s E s O J s E
117 53 70 114 116 syl3anc K HL W H f T s E s O J s E
118 1 9 11 tendocl K HL W H J s E f T J s f T
119 53 117 68 118 syl3anc K HL W H f T s E s O J s f T
120 6 7 1 8 lhpocnel2 K HL W H P C ¬ P ˙ W
121 53 120 syl K HL W H f T s E s O P C ¬ P ˙ W
122 6 7 1 9 ltrnel K HL W H J s f T P C ¬ P ˙ W J s f P C ¬ J s f P ˙ W
123 53 119 121 122 syl3anc K HL W H f T s E s O J s f P C ¬ J s f P ˙ W
124 eqid DIsoC K W = DIsoC K W
125 6 7 1 124 3 dihvalcqat K HL W H J s f P C ¬ J s f P ˙ W I J s f P = DIsoC K W J s f P
126 53 123 125 syl2anc K HL W H f T s E s O I J s f P = DIsoC K W J s f P
127 6 7 1 8 9 11 124 20 dicval2 K HL W H J s f P C ¬ J s f P ˙ W DIsoC K W J s f P = g r | g = r G r E
128 53 123 127 syl2anc K HL W H f T s E s O DIsoC K W J s f P = g r | g = r G r E
129 126 128 eqtrd K HL W H f T s E s O I J s f P = g r | g = r G r E
130 108 113 129 3eqtr4d K HL W H f T s E s O N f s = I J s f P
131 5 1 3 dihfn K HL W H I Fn B
132 131 adantr K HL W H f T s E I Fn B
133 132 adantr K HL W H f T s E s O I Fn B
134 simplll K HL W H f T s E s O K HL
135 hlop K HL K OP
136 134 135 syl K HL W H f T s E s O K OP
137 5 1 lhpbase W H W B
138 137 ad3antlr K HL W H f T s E s O W B
139 eqid oc K = oc K
140 5 139 opoccl K OP W B oc K W B
141 136 138 140 syl2anc K HL W H f T s E s O oc K W B
142 8 141 eqeltrid K HL W H f T s E s O P B
143 5 1 9 ltrncl K HL W H J s f T P B J s f P B
144 53 119 142 143 syl3anc K HL W H f T s E s O J s f P B
145 fnfvelrn I Fn B J s f P B I J s f P ran I
146 133 144 145 syl2anc K HL W H f T s E s O I J s f P ran I
147 130 146 eqeltrd K HL W H f T s E s O N f s ran I
148 52 147 pm2.61dane K HL W H f T s E N f s ran I
149 148 ralrimivva K HL W H f T s E N f s ran I
150 sneq v = f s v = f s
151 150 fveq2d v = f s N v = N f s
152 151 eleq1d v = f s N v ran I N f s ran I
153 152 ralxp v T × E N v ran I f T s E N f s ran I
154 149 153 sylibr K HL W H v T × E N v ran I
155 154 r19.21bi K HL W H v T × E N v ran I
156 30 155 syldan K HL W H v V 0 ˙ N v ran I
157 eleq1a N v ran I D = N v D ran I
158 156 157 syl K HL W H v V 0 ˙ D = N v D ran I
159 158 rexlimdva K HL W H v V 0 ˙ D = N v D ran I
160 159 adantr K HL W H D A v V 0 ˙ D = N v D ran I
161 25 160 mpd K HL W H D A D ran I