# Metamath Proof Explorer

## Theorem baerlem5blem1

Description: Lemma for baerlem5b . (Contributed by NM, 9-Apr-2015)

Ref Expression
Hypotheses baerlem3.v $⊢ V = Base W$
baerlem3.m
baerlem3.o
baerlem3.s
baerlem3.n $⊢ N = LSpan ⁡ W$
baerlem3.w $⊢ φ → W ∈ LVec$
baerlem3.x $⊢ φ → X ∈ V$
baerlem3.c $⊢ φ → ¬ X ∈ N ⁡ Y Z$
baerlem3.d $⊢ φ → N ⁡ Y ≠ N ⁡ Z$
baerlem3.y
baerlem3.z
baerlem3.p
baerlem3.t
baerlem3.r $⊢ R = Scalar ⁡ W$
baerlem3.b $⊢ B = Base R$
baerlem3.a
baerlem3.l $⊢ L = - R$
baerlem3.q $⊢ Q = 0 R$
baerlem3.i $⊢ I = inv g ⁡ R$
baerlem5b.a1 $⊢ φ → a ∈ B$
baerlem5b.b1 $⊢ φ → b ∈ B$
baerlem5b.d1 $⊢ φ → d ∈ B$
baerlem5b.e1 $⊢ φ → e ∈ B$
baerlem5b.j1
baerlem5b.j2
Assertion baerlem5blem1

### Proof

Step Hyp Ref Expression
1 baerlem3.v $⊢ V = Base W$
2 baerlem3.m
3 baerlem3.o
4 baerlem3.s
5 baerlem3.n $⊢ N = LSpan ⁡ W$
6 baerlem3.w $⊢ φ → W ∈ LVec$
7 baerlem3.x $⊢ φ → X ∈ V$
8 baerlem3.c $⊢ φ → ¬ X ∈ N ⁡ Y Z$
9 baerlem3.d $⊢ φ → N ⁡ Y ≠ N ⁡ Z$
10 baerlem3.y
11 baerlem3.z
12 baerlem3.p
13 baerlem3.t
14 baerlem3.r $⊢ R = Scalar ⁡ W$
15 baerlem3.b $⊢ B = Base R$
16 baerlem3.a
17 baerlem3.l $⊢ L = - R$
18 baerlem3.q $⊢ Q = 0 R$
19 baerlem3.i $⊢ I = inv g ⁡ R$
20 baerlem5b.a1 $⊢ φ → a ∈ B$
21 baerlem5b.b1 $⊢ φ → b ∈ B$
22 baerlem5b.d1 $⊢ φ → d ∈ B$
23 baerlem5b.e1 $⊢ φ → e ∈ B$
24 baerlem5b.j1
25 baerlem5b.j2
26 eqid $⊢ LSubSp ⁡ W = LSubSp ⁡ W$
27 lveclmod $⊢ W ∈ LVec → W ∈ LMod$
28 6 27 syl $⊢ φ → W ∈ LMod$
29 10 eldifad $⊢ φ → Y ∈ V$
30 11 eldifad $⊢ φ → Z ∈ V$
31 1 26 5 28 29 30 lspprcl $⊢ φ → N ⁡ Y Z ∈ LSubSp ⁡ W$
32 1 12 13 14 15 5 28 20 21 29 30 lsppreli
33 14 lmodring $⊢ W ∈ LMod → R ∈ Ring$
34 28 33 syl $⊢ φ → R ∈ Ring$
35 ringgrp $⊢ R ∈ Ring → R ∈ Grp$
36 34 35 syl $⊢ φ → R ∈ Grp$
37 15 19 grpinvcl $⊢ R ∈ Grp ∧ d ∈ B → I ⁡ d ∈ B$
38 36 22 37 syl2anc $⊢ φ → I ⁡ d ∈ B$
39 1 12 13 14 15 5 28 38 38 29 30 lsppreli
40 14 15 18 lmod0cl $⊢ W ∈ LMod → Q ∈ B$
41 28 40 syl $⊢ φ → Q ∈ B$
42 14 15 16 lmodacl
43 28 22 23 42 syl3anc
44 1 14 13 15 lmodvscl
45 28 20 29 44 syl3anc
46 1 14 13 15 lmodvscl
47 28 21 30 46 syl3anc
48 1 12 lmodvacl
49 28 45 47 48 syl3anc
50 1 12 3 lmod0vlid
51 28 49 50 syl2anc
52 1 14 13 18 3 lmod0vs
53 28 7 52 syl2anc
54 53 oveq1d
55 51 54 24 3eqtr4d
56 1 12 lmodvacl
57 28 29 30 56 syl3anc
58 1 13 14 15 2 28 22 7 57 lmodsubdi
59 1 14 13 15 lmodvscl
60 28 22 7 59 syl3anc
61 1 12 2 13 14 15 19 28 22 60 57 lmodsubvs
62 1 12 14 13 15 lmodvsdi
63 28 38 29 30 62 syl13anc
64 63 oveq2d
65 58 61 64 3eqtrd
66 65 oveq1d
67 1 12 14 13 15 16 lmodvsdir
68 28 22 23 7 67 syl13anc
69 68 oveq1d
70 lmodabl $⊢ W ∈ LMod → W ∈ Abel$
71 28 70 syl $⊢ φ → W ∈ Abel$
72 1 14 13 15 lmodvscl
73 28 23 7 72 syl3anc
74 1 14 13 15 lmodvscl
75 28 38 29 74 syl3anc
76 1 14 13 15 lmodvscl
77 28 38 30 76 syl3anc
78 1 12 lmodvacl
79 28 75 77 78 syl3anc
80 1 12 71 60 73 79 abl32
81 69 80 eqtrd
82 66 25 81 3eqtr4d
83 55 82 eqtrd
84 1 12 14 15 13 26 6 31 7 8 32 39 41 43 83 lvecindp
85 84 simpld
86 85 oveq1d
87 86 53 eqtr3d
88 87 oveq1d
89 1 12 3 lmod0vlid
90 28 79 89 syl2anc
91 88 90 eqtrd
92 91 82 63 3eqtr4d