# Metamath Proof Explorer

## Theorem lcfrlem29

Description: Lemma for lcfr . (Contributed by NM, 9-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcfrlem17.o
lcfrlem17.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcfrlem17.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
lcfrlem17.p
lcfrlem17.z
lcfrlem17.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
lcfrlem17.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
lcfrlem17.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lcfrlem17.x
lcfrlem17.y
lcfrlem17.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
lcfrlem22.b
lcfrlem24.t
lcfrlem24.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
lcfrlem24.q ${⊢}{Q}={0}_{{S}}$
lcfrlem24.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
lcfrlem24.j
lcfrlem24.ib ${⊢}{\phi }\to {I}\in {B}$
lcfrlem24.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
lcfrlem25.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
lcfrlem28.jn ${⊢}{\phi }\to {J}\left({Y}\right)\left({I}\right)\ne {Q}$
lcfrlem29.i ${⊢}{F}={inv}_{r}\left({S}\right)$
Assertion lcfrlem29 ${⊢}{\phi }\to {F}\left({J}\left({Y}\right)\left({I}\right)\right){\cdot }_{{S}}{J}\left({X}\right)\left({I}\right)\in {R}$

### Proof

Step Hyp Ref Expression
1 lcfrlem17.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcfrlem17.o
3 lcfrlem17.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 lcfrlem17.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 lcfrlem17.p
6 lcfrlem17.z
7 lcfrlem17.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 lcfrlem17.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
9 lcfrlem17.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 lcfrlem17.x
11 lcfrlem17.y
12 lcfrlem17.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
13 lcfrlem22.b
14 lcfrlem24.t
15 lcfrlem24.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
16 lcfrlem24.q ${⊢}{Q}={0}_{{S}}$
17 lcfrlem24.r ${⊢}{R}={\mathrm{Base}}_{{S}}$
18 lcfrlem24.j
19 lcfrlem24.ib ${⊢}{\phi }\to {I}\in {B}$
20 lcfrlem24.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
21 lcfrlem25.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
22 lcfrlem28.jn ${⊢}{\phi }\to {J}\left({Y}\right)\left({I}\right)\ne {Q}$
23 lcfrlem29.i ${⊢}{F}={inv}_{r}\left({S}\right)$
24 1 3 9 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
25 15 lmodring ${⊢}{U}\in \mathrm{LMod}\to {S}\in \mathrm{Ring}$
26 24 25 syl ${⊢}{\phi }\to {S}\in \mathrm{Ring}$
27 1 3 9 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
28 15 lvecdrng ${⊢}{U}\in \mathrm{LVec}\to {S}\in \mathrm{DivRing}$
29 27 28 syl ${⊢}{\phi }\to {S}\in \mathrm{DivRing}$
30 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
31 eqid ${⊢}{0}_{{D}}={0}_{{D}}$
32 eqid
33 1 2 3 4 5 14 15 17 6 30 20 21 31 32 18 9 11 lcfrlem10 ${⊢}{\phi }\to {J}\left({Y}\right)\in \mathrm{LFnl}\left({U}\right)$
34 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
35 1 2 3 4 5 6 7 8 9 10 11 12 13 lcfrlem22 ${⊢}{\phi }\to {B}\in {A}$
36 34 8 24 35 lsatlssel ${⊢}{\phi }\to {B}\in \mathrm{LSubSp}\left({U}\right)$
37 4 34 lssel ${⊢}\left({B}\in \mathrm{LSubSp}\left({U}\right)\wedge {I}\in {B}\right)\to {I}\in {V}$
38 36 19 37 syl2anc ${⊢}{\phi }\to {I}\in {V}$
39 15 17 4 30 lflcl ${⊢}\left({U}\in \mathrm{LMod}\wedge {J}\left({Y}\right)\in \mathrm{LFnl}\left({U}\right)\wedge {I}\in {V}\right)\to {J}\left({Y}\right)\left({I}\right)\in {R}$
40 24 33 38 39 syl3anc ${⊢}{\phi }\to {J}\left({Y}\right)\left({I}\right)\in {R}$
41 17 16 23 drnginvrcl ${⊢}\left({S}\in \mathrm{DivRing}\wedge {J}\left({Y}\right)\left({I}\right)\in {R}\wedge {J}\left({Y}\right)\left({I}\right)\ne {Q}\right)\to {F}\left({J}\left({Y}\right)\left({I}\right)\right)\in {R}$
42 29 40 22 41 syl3anc ${⊢}{\phi }\to {F}\left({J}\left({Y}\right)\left({I}\right)\right)\in {R}$
43 1 2 3 4 5 14 15 17 6 30 20 21 31 32 18 9 10 lcfrlem10 ${⊢}{\phi }\to {J}\left({X}\right)\in \mathrm{LFnl}\left({U}\right)$
44 15 17 4 30 lflcl ${⊢}\left({U}\in \mathrm{LMod}\wedge {J}\left({X}\right)\in \mathrm{LFnl}\left({U}\right)\wedge {I}\in {V}\right)\to {J}\left({X}\right)\left({I}\right)\in {R}$
45 24 43 38 44 syl3anc ${⊢}{\phi }\to {J}\left({X}\right)\left({I}\right)\in {R}$
46 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
47 17 46 ringcl ${⊢}\left({S}\in \mathrm{Ring}\wedge {F}\left({J}\left({Y}\right)\left({I}\right)\right)\in {R}\wedge {J}\left({X}\right)\left({I}\right)\in {R}\right)\to {F}\left({J}\left({Y}\right)\left({I}\right)\right){\cdot }_{{S}}{J}\left({X}\right)\left({I}\right)\in {R}$
48 26 42 45 47 syl3anc ${⊢}{\phi }\to {F}\left({J}\left({Y}\right)\left({I}\right)\right){\cdot }_{{S}}{J}\left({X}\right)\left({I}\right)\in {R}$