# Metamath Proof Explorer

## Theorem lcfrlem29

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

Ref Expression
Hypotheses lcfrlem17.h
`|- H = ( LHyp ` K )`
lcfrlem17.o
`|- ._|_ = ( ( ocH ` K ) ` W )`
lcfrlem17.u
`|- U = ( ( DVecH ` K ) ` W )`
lcfrlem17.v
`|- V = ( Base ` U )`
lcfrlem17.p
`|- .+ = ( +g ` U )`
lcfrlem17.z
`|- .0. = ( 0g ` U )`
lcfrlem17.n
`|- N = ( LSpan ` U )`
lcfrlem17.a
`|- A = ( LSAtoms ` U )`
lcfrlem17.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
lcfrlem17.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
lcfrlem17.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
lcfrlem17.ne
`|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
lcfrlem22.b
`|- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )`
lcfrlem24.t
`|- .x. = ( .s ` U )`
lcfrlem24.s
`|- S = ( Scalar ` U )`
lcfrlem24.q
`|- Q = ( 0g ` S )`
lcfrlem24.r
`|- R = ( Base ` S )`
lcfrlem24.j
`|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )`
lcfrlem24.ib
`|- ( ph -> I e. B )`
lcfrlem24.l
`|- L = ( LKer ` U )`
lcfrlem25.d
`|- D = ( LDual ` U )`
lcfrlem28.jn
`|- ( ph -> ( ( J ` Y ) ` I ) =/= Q )`
lcfrlem29.i
`|- F = ( invr ` S )`
Assertion lcfrlem29
`|- ( ph -> ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) e. R )`

### Proof

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