Metamath Proof Explorer


Theorem lcfrlem27

Description: Lemma for lcfr . Special case of lcfrlem37 when ( ( JY )I ) is zero. (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h H = LHyp K
lcfrlem17.o ˙ = ocH K W
lcfrlem17.u U = DVecH K W
lcfrlem17.v V = Base U
lcfrlem17.p + ˙ = + U
lcfrlem17.z 0 ˙ = 0 U
lcfrlem17.n N = LSpan U
lcfrlem17.a A = LSAtoms U
lcfrlem17.k φ K HL W H
lcfrlem17.x φ X V 0 ˙
lcfrlem17.y φ Y V 0 ˙
lcfrlem17.ne φ N X N Y
lcfrlem22.b B = N X Y ˙ X + ˙ Y
lcfrlem24.t · ˙ = U
lcfrlem24.s S = Scalar U
lcfrlem24.q Q = 0 S
lcfrlem24.r R = Base S
lcfrlem24.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
lcfrlem24.ib φ I B
lcfrlem24.l L = LKer U
lcfrlem25.d D = LDual U
lcfrlem25.jz φ J Y I = Q
lcfrlem25.in φ I 0 ˙
lcfrlem27.g φ G LSubSp D
lcfrlem27.gs φ G f LFnl U | ˙ ˙ L f = L f
lcfrlem27.e E = g G ˙ L g
lcfrlem27.xe φ X E
lcfrlem27.ye φ Y E
Assertion lcfrlem27 φ X + ˙ Y E

Proof

Step Hyp Ref Expression
1 lcfrlem17.h H = LHyp K
2 lcfrlem17.o ˙ = ocH K W
3 lcfrlem17.u U = DVecH K W
4 lcfrlem17.v V = Base U
5 lcfrlem17.p + ˙ = + U
6 lcfrlem17.z 0 ˙ = 0 U
7 lcfrlem17.n N = LSpan U
8 lcfrlem17.a A = LSAtoms U
9 lcfrlem17.k φ K HL W H
10 lcfrlem17.x φ X V 0 ˙
11 lcfrlem17.y φ Y V 0 ˙
12 lcfrlem17.ne φ N X N Y
13 lcfrlem22.b B = N X Y ˙ X + ˙ Y
14 lcfrlem24.t · ˙ = U
15 lcfrlem24.s S = Scalar U
16 lcfrlem24.q Q = 0 S
17 lcfrlem24.r R = Base S
18 lcfrlem24.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
19 lcfrlem24.ib φ I B
20 lcfrlem24.l L = LKer U
21 lcfrlem25.d D = LDual U
22 lcfrlem25.jz φ J Y I = Q
23 lcfrlem25.in φ I 0 ˙
24 lcfrlem27.g φ G LSubSp D
25 lcfrlem27.gs φ G f LFnl U | ˙ ˙ L f = L f
26 lcfrlem27.e E = g G ˙ L g
27 lcfrlem27.xe φ X E
28 lcfrlem27.ye φ Y E
29 eqid LFnl U = LFnl U
30 eqid 0 D = 0 D
31 eqid f LFnl U | ˙ ˙ L f = L f = f LFnl U | ˙ ˙ L f = L f
32 eqid LSubSp D = LSubSp D
33 eldifsni Y V 0 ˙ Y 0 ˙
34 11 33 syl φ Y 0 ˙
35 eldifsn Y E 0 ˙ Y E Y 0 ˙
36 28 34 35 sylanbrc φ Y E 0 ˙
37 1 2 3 4 5 14 15 17 6 29 20 21 30 31 18 9 32 24 25 26 36 lcfrlem16 φ J Y G
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 lcfrlem26 φ X + ˙ Y ˙ L J Y
39 2fveq3 g = J Y ˙ L g = ˙ L J Y
40 39 eleq2d g = J Y X + ˙ Y ˙ L g X + ˙ Y ˙ L J Y
41 40 rspcev J Y G X + ˙ Y ˙ L J Y g G X + ˙ Y ˙ L g
42 37 38 41 syl2anc φ g G X + ˙ Y ˙ L g
43 eliun X + ˙ Y g G ˙ L g g G X + ˙ Y ˙ L g
44 42 43 sylibr φ X + ˙ Y g G ˙ L g
45 44 26 eleqtrrdi φ X + ˙ Y E