Metamath Proof Explorer


Theorem lcfrlem3

Description: Lemma for lcfr . (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses lcfrlem1.v V = Base U
lcfrlem1.s S = Scalar U
lcfrlem1.q × ˙ = S
lcfrlem1.z 0 ˙ = 0 S
lcfrlem1.i I = inv r S
lcfrlem1.f F = LFnl U
lcfrlem1.d D = LDual U
lcfrlem1.t · ˙ = D
lcfrlem1.m - ˙ = - D
lcfrlem1.u φ U LVec
lcfrlem1.e φ E F
lcfrlem1.g φ G F
lcfrlem1.x φ X V
lcfrlem1.n φ G X 0 ˙
lcfrlem1.h H = E - ˙ I G X × ˙ E X · ˙ G
lcfrlem2.l L = LKer U
Assertion lcfrlem3 φ X L H

Proof

Step Hyp Ref Expression
1 lcfrlem1.v V = Base U
2 lcfrlem1.s S = Scalar U
3 lcfrlem1.q × ˙ = S
4 lcfrlem1.z 0 ˙ = 0 S
5 lcfrlem1.i I = inv r S
6 lcfrlem1.f F = LFnl U
7 lcfrlem1.d D = LDual U
8 lcfrlem1.t · ˙ = D
9 lcfrlem1.m - ˙ = - D
10 lcfrlem1.u φ U LVec
11 lcfrlem1.e φ E F
12 lcfrlem1.g φ G F
13 lcfrlem1.x φ X V
14 lcfrlem1.n φ G X 0 ˙
15 lcfrlem1.h H = E - ˙ I G X × ˙ E X · ˙ G
16 lcfrlem2.l L = LKer U
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lcfrlem1 φ H X = 0 ˙
18 lveclmod U LVec U LMod
19 10 18 syl φ U LMod
20 eqid Base S = Base S
21 2 lmodring U LMod S Ring
22 19 21 syl φ S Ring
23 2 lvecdrng U LVec S DivRing
24 10 23 syl φ S DivRing
25 2 20 1 6 lflcl U LVec G F X V G X Base S
26 10 12 13 25 syl3anc φ G X Base S
27 20 4 5 drnginvrcl S DivRing G X Base S G X 0 ˙ I G X Base S
28 24 26 14 27 syl3anc φ I G X Base S
29 2 20 1 6 lflcl U LVec E F X V E X Base S
30 10 11 13 29 syl3anc φ E X Base S
31 20 3 ringcl S Ring I G X Base S E X Base S I G X × ˙ E X Base S
32 22 28 30 31 syl3anc φ I G X × ˙ E X Base S
33 6 2 20 7 8 19 32 12 ldualvscl φ I G X × ˙ E X · ˙ G F
34 6 7 9 19 11 33 ldualvsubcl φ E - ˙ I G X × ˙ E X · ˙ G F
35 15 34 eqeltrid φ H F
36 1 2 4 6 16 10 35 13 ellkr2 φ X L H H X = 0 ˙
37 17 36 mpbird φ X L H