Metamath Proof Explorer


Theorem lcfrlem41

Description: Lemma for lcfr . Eliminate span condition. (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 ˙
Assertion lcfrlem41 φ 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 eqid LSpan U = LSpan U
20 11 adantr φ LSpan U X = LSpan U Y K HL W H
21 12 adantr φ LSpan U X = LSpan U Y G Q
22 14 adantr φ LSpan U X = LSpan U Y X E
23 15 adantr φ LSpan U X = LSpan U Y Y E
24 simpr φ LSpan U X = LSpan U Y LSpan U X = LSpan U Y
25 1 2 3 4 19 6 7 8 20 21 10 22 23 24 lcfrlem6 φ LSpan U X = LSpan U Y X + ˙ Y E
26 11 adantr φ LSpan U X LSpan U Y K HL W H
27 12 adantr φ LSpan U X LSpan U Y G Q
28 13 adantr φ LSpan U X LSpan U Y G C
29 14 adantr φ LSpan U X LSpan U Y X E
30 15 adantr φ LSpan U X LSpan U Y Y E
31 17 adantr φ LSpan U X LSpan U Y X 0 ˙
32 18 adantr φ LSpan U X LSpan U Y Y 0 ˙
33 simpr φ LSpan U X LSpan U Y LSpan U X LSpan U Y
34 1 2 3 4 5 6 7 8 9 10 26 27 28 29 30 16 31 32 19 33 lcfrlem40 φ LSpan U X LSpan U Y X + ˙ Y E
35 25 34 pm2.61dane φ X + ˙ Y E