Metamath Proof Explorer

Theorem baerlem5blem2

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

Ref Expression
Hypotheses baerlem3.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
baerlem3.m
baerlem3.o
baerlem3.s
baerlem3.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
baerlem3.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
baerlem3.x ${⊢}{\phi }\to {X}\in {V}$
baerlem3.c ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
baerlem3.d ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
baerlem3.y
baerlem3.z
baerlem3.p
baerlem3.t
baerlem3.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
baerlem3.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
baerlem3.a
baerlem3.l ${⊢}{L}={-}_{{R}}$
baerlem3.q ${⊢}{Q}={0}_{{R}}$
baerlem3.i ${⊢}{I}={inv}_{g}\left({R}\right)$
Assertion baerlem5blem2

Proof

Step Hyp Ref Expression
1 baerlem3.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 baerlem3.m
3 baerlem3.o
4 baerlem3.s
5 baerlem3.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
6 baerlem3.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
7 baerlem3.x ${⊢}{\phi }\to {X}\in {V}$
8 baerlem3.c ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
9 baerlem3.d ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
10 baerlem3.y
11 baerlem3.z
12 baerlem3.p
13 baerlem3.t
14 baerlem3.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
15 baerlem3.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
16 baerlem3.a
17 baerlem3.l ${⊢}{L}={-}_{{R}}$
18 baerlem3.q ${⊢}{Q}={0}_{{R}}$
19 baerlem3.i ${⊢}{I}={inv}_{g}\left({R}\right)$
20 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
21 6 20 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
22 10 eldifad ${⊢}{\phi }\to {Y}\in {V}$
23 11 eldifad ${⊢}{\phi }\to {Z}\in {V}$
24 1 12 5 4 lspsntri
25 21 22 23 24 syl3anc
26 1 12 lmodvacl
27 21 22 23 26 syl3anc
28 1 2 lmodvsubcl
29 21 7 27 28 syl3anc
30 1 2 5 21 29 7 lspsnsub
31 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
32 21 31 syl ${⊢}{\phi }\to {W}\in \mathrm{Abel}$
33 1 2 32 7 27 ablnncan
34 33 sneqd
35 34 fveq2d
36 30 35 eqtrd
37 1 2 4 5 lspsntrim
38 21 29 7 37 syl3anc
39 36 38 eqsstrrd
40 25 39 ssind
41 elin
42 1 12 14 15 13 4 5 21 22 23 lsmspsn
43 1 12 14 15 13 4 5 21 29 7 lsmspsn
44 42 43 anbi12d
45 41 44 syl5bb
46 simp11
47 46 6 syl
48 46 7 syl
49 46 8 syl
50 46 9 syl
51 46 10 syl
52 46 11 syl
53 simp12l
54 simp12r
55 simp2l
56 simp2r
57 simp13
58 simp3
59 1 2 3 4 5 47 48 49 50 51 52 12 13 14 15 16 17 18 19 53 54 55 56 57 58 baerlem5blem1
60 46 21 syl
61 14 lmodring ${⊢}{W}\in \mathrm{LMod}\to {R}\in \mathrm{Ring}$
62 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
63 46 21 61 62 4syl
64 15 19 grpinvcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {d}\in {B}\right)\to {I}\left({d}\right)\in {B}$
65 63 55 64 syl2anc
66 46 27 syl
67 1 13 14 15 5 60 65 66 lspsneli
68 59 67 eqeltrd
69 68 3exp
70 69 rexlimdvv
71 70 3exp
72 71 rexlimdvv
73 72 impd
74 45 73 sylbid
75 74 ssrdv
76 40 75 eqssd