Metamath Proof Explorer


Theorem lcfrlem39

Description: Lemma for lcfr . Eliminate J . (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
lcfrlem38.b B = N X Y ˙ X + ˙ Y
lcfrlem38.i φ I B
lcfrlem38.n φ I 0 ˙
Assertion lcfrlem39 φ 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 lcfrlem38.b B = N X Y ˙ X + ˙ Y
22 lcfrlem38.i φ I B
23 lcfrlem38.n φ I 0 ˙
24 eqid Base U = Base U
25 eqid U = U
26 eqid Scalar U = Scalar U
27 eqid Base Scalar U = Base Scalar U
28 oveq1 j = k j U x = k U x
29 28 oveq2d j = k w + ˙ j U x = w + ˙ k U x
30 29 eqeq2d j = k v = w + ˙ j U x v = w + ˙ k U x
31 30 rexbidv j = k w ˙ x v = w + ˙ j U x w ˙ x v = w + ˙ k U x
32 31 cbvriotavw ι j Base Scalar U | w ˙ x v = w + ˙ j U x = ι k Base Scalar U | w ˙ x v = w + ˙ k U x
33 32 mpteq2i v Base U ι j Base Scalar U | w ˙ x v = w + ˙ j U x = v Base U ι k Base Scalar U | w ˙ x v = w + ˙ k U x
34 33 mpteq2i x Base U 0 ˙ v Base U ι j Base Scalar U | w ˙ x v = w + ˙ j U x = x Base U 0 ˙ v Base U ι k Base Scalar U | w ˙ x v = w + ˙ k U x
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 34 lcfrlem38 φ X + ˙ Y E