Theorem lcfrlem30 35186

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

Hypotheses

Ref	Expression
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 )
lcfrlem30.m	|- .- = ( -g ` D )
lcfrlem30.c	|- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )

Assertion

Ref	Expression
lcfrlem30	|- ( ph -> C e. (LFnl ` U ) )

Distinct variable groups:   v, k, w, x, ._|_   .+ , k, v, w, x   R, k, v, x   S, k   .x. , k, v, w, x   v, V, x   k, X, v, w, x   k, Y, v, w, x   x, .0.

Allowed substitution hints:   ph( x, w, v, k)   A( x, w, v, k)   B( x, w, v, k)   C( x, w, v, k)   D( x, w, v, k)   Q( x, w, v, k)   R( w)   S( x, w, v)   U( x, w, v, k)   F( x, w, v, k)   H( x, w, v, k)   I( x, w, v, k)   J( x, w, v, k)   K( x, w, v, k)   L( x, w, v, k)   .- ( x, w, v, k)   N( x, w, v, k)   V( w, k)   W( x, w, v, k)   .0. ( w, v, k)

Proof of Theorem lcfrlem30

Step	Hyp	Ref	Expression
1		lcfrlem30.c	. 2 |- C = ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) )
2		eqid 2462	. . 3 |- (LFnl ` U ) = (LFnl ` U )
3		lcfrlem25.d	. . 3 |- D = (LDual ` U )
4		lcfrlem30.m	. . 3 |- .- = ( -g ` D )
5		lcfrlem17.h	. . . 4 |- H = ( LHyp ` K )
6		lcfrlem17.u	. . . 4 |- U = ( ( DVecH ` K ) ` W )
7		lcfrlem17.k	. . . 4 |- ( ph -> ( K e. HL /\ W e. H ) )
8	5, 6, 7	dvhlmod 34724	. . 3 |- ( ph -> U e. LMod )
9		lcfrlem17.o	. . . 4 |- ._|_ = ( ( ocH ` K ) ` W )
10		lcfrlem17.v	. . . 4 |- V = ( Base ` U )
11		lcfrlem17.p	. . . 4 |- .+ = ( +g ` U )
12		lcfrlem24.t	. . . 4 |- .x. = ( .s ` U )
13		lcfrlem24.s	. . . 4 |- S = (Scalar ` U )
14		lcfrlem24.r	. . . 4 |- R = ( Base ` S )
15		lcfrlem17.z	. . . 4 |- .0. = ( 0g ` U )
16		lcfrlem24.l	. . . 4 |- L = (LKer ` U )
17		eqid 2462	. . . 4 |- ( 0g ` D ) = ( 0g ` D )
18		eqid 2462	. . . 4 |- { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
19		lcfrlem24.j	. . . 4 |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
20		lcfrlem17.x	. . . 4 |- ( ph -> X e. ( V \ { .0. } ) )
21	5, 9, 6, 10, 11, 12, 13, 14, 15, 2, 16, 3, 17, 18, 19, 7, 20	lcfrlem10 35166	. . 3 |- ( ph -> ( J ` X ) e. (LFnl ` U ) )
22		eqid 2462	. . . 4 |- ( .s ` D ) = ( .s ` D )
23		lcfrlem17.n	. . . . 5 |- N = ( LSpan ` U )
24		lcfrlem17.a	. . . . 5 |- A = (LSAtoms ` U )
25		lcfrlem17.y	. . . . 5 |- ( ph -> Y e. ( V \ { .0. } ) )
26		lcfrlem17.ne	. . . . 5 |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
27		lcfrlem22.b	. . . . 5 |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
28		lcfrlem24.q	. . . . 5 |- Q = ( 0g ` S )
29		lcfrlem24.ib	. . . . 5 |- ( ph -> I e. B )
30		lcfrlem28.jn	. . . . 5 |- ( ph -> ( ( J ` Y ) ` I ) =/= Q )
31		lcfrlem29.i	. . . . 5 |- F = ( invr ` S )
32	5, 9, 6, 10, 11, 15, 23, 24, 7, 20, 25, 26, 27, 12, 13, 28, 14, 19, 29, 16, 3, 30, 31	lcfrlem29 35185	. . . 4 |- ( ph -> ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) e. R )
33	5, 9, 6, 10, 11, 12, 13, 14, 15, 2, 16, 3, 17, 18, 19, 7, 25	lcfrlem10 35166	. . . 4 |- ( ph -> ( J ` Y ) e. (LFnl ` U ) )
34	2, 13, 14, 3, 22, 8, 32, 33	ldualvscl 32751	. . 3 |- ( ph -> ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) e. (LFnl ` U ) )
35	2, 3, 4, 8, 21, 34	ldualvsubcl 32768	. 2 |- ( ph -> ( ( J ` X ) .- ( ( ( F ` ( ( J ` Y ) ` I ) ) ( .r ` S ) ( ( J ` X ) ` I ) ) ( .s ` D ) ( J ` Y ) ) ) e. (LFnl ` U ) )
36	1, 35	syl5eqel 2544	1 |- ( ph -> C e. (LFnl ` U ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   e. wcel 1898   =/= wne 2633   E.wrex 2750   {crab 2753   \ cdif 3413   i^i cin 3415   {csn 3980   {cpr 3982   |-> cmpt 4477   ` cfv 5605   iota_crio 6281  (class class class)co 6320   Basecbs 15176   +g cplusg 15245   .rcmulr 15246  Scalarcsca 15248   .scvsca 15249   0gc0g 15393   -gcsg 16726   invrcinvr 17954   LSpanclspn 18249  LSAtomsclsa 32586  LFnlclfn 32669  LKerclk 32697  LDualcld 32735   HLchlt 32962   LHypclh 33595   DVecHcdvh 34692   ocHcoch 34961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-riotaBAD 32571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-of 6563  df-om 6725  df-1st 6825  df-2nd 6826  df-tpos 7004  df-undef 7051  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-oadd 7217  df-er 7394  df-map 7505  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-n0 10904  df-z 10972  df-uz 11194  df-fz 11820  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-sca 15261  df-vsca 15262  df-0g 15395  df-mre 15547  df-mrc 15548  df-acs 15550  df-preset 16228  df-poset 16246  df-plt 16259  df-lub 16275  df-glb 16276  df-join 16277  df-meet 16278  df-p0 16340  df-p1 16341  df-lat 16347  df-clat 16409  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-submnd 16638  df-grp 16728  df-minusg 16729  df-sbg 16730  df-subg 16869  df-cntz 17026  df-oppg 17052  df-lsm 17343  df-cmn 17487  df-abl 17488  df-mgp 17779  df-ur 17791  df-ring 17837  df-oppr 17906  df-dvdsr 17924  df-unit 17925  df-invr 17955  df-dvr 17966  df-drng 18032  df-lmod 18148  df-lss 18211  df-lsp 18250  df-lvec 18381  df-lsatoms 32588  df-lshyp 32589  df-lcv 32631  df-lfl 32670  df-ldual 32736  df-oposet 32788  df-ol 32790  df-oml 32791  df-covers 32878  df-ats 32879  df-atl 32910  df-cvlat 32934  df-hlat 32963  df-llines 33109  df-lplanes 33110  df-lvols 33111  df-lines 33112  df-psubsp 33114  df-pmap 33115  df-padd 33407  df-lhyp 33599  df-laut 33600  df-ldil 33715  df-ltrn 33716  df-trl 33771  df-tgrp 34356  df-tendo 34368  df-edring 34370  df-dveca 34616  df-disoa 34643  df-dvech 34693  df-dib 34753  df-dic 34787  df-dih 34843  df-doch 34962  df-djh 35009

This theorem is referenced by:  lcfrlem35  35191  lcfrlem36  35192