Metamath Proof Explorer


Theorem lcfrlem38

Description: Lemma for lcfr . Combine lcfrlem27 and lcfrlem37 . (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 ˙
lcfrlem38.v V = Base U
lcfrlem38.t · ˙ = U
lcfrlem38.s S = Scalar U
lcfrlem38.r R = Base S
lcfrlem38.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
Assertion lcfrlem38 φ 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 lcfrlem38.v V = Base U
25 lcfrlem38.t · ˙ = U
26 lcfrlem38.s S = Scalar U
27 lcfrlem38.r R = Base S
28 lcfrlem38.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
29 eqid LSAtoms U = LSAtoms U
30 11 adantr φ J Y I = 0 S K HL W H
31 1 2 3 24 6 7 8 10 11 12 14 lcfrlem4 φ X V
32 eldifsn X V 0 ˙ X V X 0 ˙
33 31 17 32 sylanbrc φ X V 0 ˙
34 33 adantr φ J Y I = 0 S X V 0 ˙
35 1 2 3 24 6 7 8 10 11 12 15 lcfrlem4 φ Y V
36 eldifsn Y V 0 ˙ Y V Y 0 ˙
37 35 18 36 sylanbrc φ Y V 0 ˙
38 37 adantr φ J Y I = 0 S Y V 0 ˙
39 20 adantr φ J Y I = 0 S N X N Y
40 eqid 0 S = 0 S
41 22 adantr φ J Y I = 0 S I B
42 simpr φ J Y I = 0 S J Y I = 0 S
43 23 adantr φ J Y I = 0 S I 0 ˙
44 12 8 eleqtrdi φ G LSubSp D
45 44 adantr φ J Y I = 0 S G LSubSp D
46 13 9 sseqtrdi φ G f LFnl U | ˙ ˙ L f = L f
47 46 adantr φ J Y I = 0 S G f LFnl U | ˙ ˙ L f = L f
48 14 adantr φ J Y I = 0 S X E
49 15 adantr φ J Y I = 0 S Y E
50 1 2 3 24 4 16 19 29 30 34 38 39 21 25 26 40 27 28 41 6 7 42 43 45 47 10 48 49 lcfrlem27 φ J Y I = 0 S X + ˙ Y E
51 11 adantr φ J Y I 0 S K HL W H
52 33 adantr φ J Y I 0 S X V 0 ˙
53 37 adantr φ J Y I 0 S Y V 0 ˙
54 20 adantr φ J Y I 0 S N X N Y
55 22 adantr φ J Y I 0 S I B
56 simpr φ J Y I 0 S J Y I 0 S
57 eqid inv r S = inv r S
58 eqid - D = - D
59 eqid J X - D inv r S J Y I S J X I D J Y = J X - D inv r S J Y I S J X I D J Y
60 44 adantr φ J Y I 0 S G LSubSp D
61 46 adantr φ J Y I 0 S G f LFnl U | ˙ ˙ L f = L f
62 14 adantr φ J Y I 0 S X E
63 15 adantr φ J Y I 0 S Y E
64 1 2 3 24 4 16 19 29 51 52 53 54 21 25 26 40 27 28 55 6 7 56 57 58 59 60 61 10 62 63 lcfrlem37 φ J Y I 0 S X + ˙ Y E
65 50 64 pm2.61dane φ X + ˙ Y E