Metamath Proof Explorer


Theorem mapdordlem1a

Description: Lemma for mapdord . (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdordlem1a.h H = LHyp K
mapdordlem1a.o O = ocH K W
mapdordlem1a.u U = DVecH K W
mapdordlem1a.v V = Base U
mapdordlem1a.y Y = LSHyp U
mapdordlem1a.f F = LFnl U
mapdordlem1a.l L = LKer U
mapdordlem1a.t T = g F | O O L g Y
mapdordlem1a.c C = g F | O O L g = L g
mapdordlem1a.k φ K HL W H
Assertion mapdordlem1a φ J T J C O O L J Y

Proof

Step Hyp Ref Expression
1 mapdordlem1a.h H = LHyp K
2 mapdordlem1a.o O = ocH K W
3 mapdordlem1a.u U = DVecH K W
4 mapdordlem1a.v V = Base U
5 mapdordlem1a.y Y = LSHyp U
6 mapdordlem1a.f F = LFnl U
7 mapdordlem1a.l L = LKer U
8 mapdordlem1a.t T = g F | O O L g Y
9 mapdordlem1a.c C = g F | O O L g = L g
10 mapdordlem1a.k φ K HL W H
11 simprr φ J F O O L J Y O O L J Y
12 10 adantr φ J F O O L J Y K HL W H
13 simprl φ J F O O L J Y J F
14 1 2 3 6 5 7 12 13 dochlkr φ J F O O L J Y O O L J Y O O L J = L J L J Y
15 11 14 mpbid φ J F O O L J Y O O L J = L J L J Y
16 15 simpld φ J F O O L J Y O O L J = L J
17 16 ex φ J F O O L J Y O O L J = L J
18 17 pm4.71rd φ J F O O L J Y O O L J = L J J F O O L J Y
19 2fveq3 g = J O L g = O L J
20 19 fveq2d g = J O O L g = O O L J
21 20 eleq1d g = J O O L g Y O O L J Y
22 21 8 elrab2 J T J F O O L J Y
23 9 lcfl1lem J C J F O O L J = L J
24 23 anbi1i J C O O L J Y J F O O L J = L J O O L J Y
25 anass J F O O L J = L J O O L J Y J F O O L J = L J O O L J Y
26 an12 J F O O L J = L J O O L J Y O O L J = L J J F O O L J Y
27 24 25 26 3bitri J C O O L J Y O O L J = L J J F O O L J Y
28 18 22 27 3bitr4g φ J T J C O O L J Y