Metamath Proof Explorer


Theorem lcfrlem40

Description: Lemma for lcfr . Eliminate B and I . (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem38.h H = LHyp K
lcfrlem38.o ˙ = ocH K W
lcfrlem38.u U = DVecH K W
lcfrlem38.p + ˙ = + U
lcfrlem38.f F = LFnl U
lcfrlem38.l L = LKer U
lcfrlem38.d D = LDual U
lcfrlem38.q Q = LSubSp D
lcfrlem38.c C = f LFnl U | ˙ ˙ L f = L f
lcfrlem38.e E = g G ˙ L g
lcfrlem38.k φ K HL W H
lcfrlem38.g φ G Q
lcfrlem38.gs φ G C
lcfrlem38.xe φ X E
lcfrlem38.ye φ Y E
lcfrlem38.z 0 ˙ = 0 U
lcfrlem38.x φ X 0 ˙
lcfrlem38.y φ Y 0 ˙
lcfrlem38.sp N = LSpan U
lcfrlem38.ne φ N X N Y
Assertion lcfrlem40 φ X + ˙ Y E

Proof

Step Hyp Ref Expression
1 lcfrlem38.h H = LHyp K
2 lcfrlem38.o ˙ = ocH K W
3 lcfrlem38.u U = DVecH K W
4 lcfrlem38.p + ˙ = + U
5 lcfrlem38.f F = LFnl U
6 lcfrlem38.l L = LKer U
7 lcfrlem38.d D = LDual U
8 lcfrlem38.q Q = LSubSp D
9 lcfrlem38.c C = f LFnl U | ˙ ˙ L f = L f
10 lcfrlem38.e E = g G ˙ L g
11 lcfrlem38.k φ K HL W H
12 lcfrlem38.g φ G Q
13 lcfrlem38.gs φ G C
14 lcfrlem38.xe φ X E
15 lcfrlem38.ye φ Y E
16 lcfrlem38.z 0 ˙ = 0 U
17 lcfrlem38.x φ X 0 ˙
18 lcfrlem38.y φ Y 0 ˙
19 lcfrlem38.sp N = LSpan U
20 lcfrlem38.ne φ N X N Y
21 eqid LSAtoms U = LSAtoms U
22 1 3 11 dvhlmod φ U LMod
23 eqid Base U = Base U
24 1 2 3 23 6 7 8 10 11 12 14 lcfrlem4 φ X Base U
25 eldifsn X Base U 0 ˙ X Base U X 0 ˙
26 24 17 25 sylanbrc φ X Base U 0 ˙
27 1 2 3 23 6 7 8 10 11 12 15 lcfrlem4 φ Y Base U
28 eldifsn Y Base U 0 ˙ Y Base U Y 0 ˙
29 27 18 28 sylanbrc φ Y Base U 0 ˙
30 1 2 3 23 4 16 19 21 11 26 29 20 lcfrlem21 φ N X Y ˙ X + ˙ Y LSAtoms U
31 16 21 22 30 lsateln0 φ i N X Y ˙ X + ˙ Y i 0 ˙
32 11 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ K HL W H
33 12 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ G Q
34 13 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ G C
35 14 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ X E
36 15 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ Y E
37 17 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ X 0 ˙
38 18 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ Y 0 ˙
39 20 3ad2ant1 φ i N X Y ˙ X + ˙ Y i 0 ˙ N X N Y
40 eqid N X Y ˙ X + ˙ Y = N X Y ˙ X + ˙ Y
41 simp2 φ i N X Y ˙ X + ˙ Y i 0 ˙ i N X Y ˙ X + ˙ Y
42 simp3 φ i N X Y ˙ X + ˙ Y i 0 ˙ i 0 ˙
43 1 2 3 4 5 6 7 8 9 10 32 33 34 35 36 16 37 38 19 39 40 41 42 lcfrlem39 φ i N X Y ˙ X + ˙ Y i 0 ˙ X + ˙ Y E
44 43 rexlimdv3a φ i N X Y ˙ X + ˙ Y i 0 ˙ X + ˙ Y E
45 31 44 mpd φ X + ˙ Y E