Theorem lcfrlem25 35136

Description: Lemma for lcfr 35154. Special case of lcfrlem35 35146 when ( ( J ` Y ) ` I ) is zero. (Contributed by NM, 11-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 )
lcfrlem25.jz	|- ( ph -> ( ( J ` Y ) ` I ) = Q )
lcfrlem25.in	|- ( ph -> I =/= .0. )

Assertion

Ref	Expression
lcfrlem25	|- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) = ( L ` ( J ` Y ) ) )

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)   D( x, w, v, k)   Q( x, w, v, k)   R( w)   S( x, w, v)   U( 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)   N( x, w, v, k)   V( w, k)   W( x, w, v, k)   .0. ( w, v, k)

Proof of Theorem lcfrlem25

Dummy variable f is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lcfrlem17.h	. . . 4 |- H = ( LHyp ` K )
2		lcfrlem17.o	. . . 4 |- ._|_ = ( ( ocH ` K ) ` W )
3		lcfrlem17.u	. . . 4 |- U = ( ( DVecH ` K ) ` W )
4		lcfrlem17.v	. . . 4 |- V = ( Base ` U )
5		lcfrlem17.p	. . . 4 |- .+ = ( +g ` U )
6		lcfrlem17.z	. . . 4 |- .0. = ( 0g ` U )
7		lcfrlem17.n	. . . 4 |- N = ( LSpan ` U )
8		lcfrlem17.a	. . . 4 |- A = (LSAtoms ` U )
9		lcfrlem17.k	. . . 4 |- ( ph -> ( K e. HL /\ W e. H ) )
10		lcfrlem17.x	. . . 4 |- ( ph -> X e. ( V \ { .0. } ) )
11		lcfrlem17.y	. . . 4 |- ( ph -> Y e. ( V \ { .0. } ) )
12		lcfrlem17.ne	. . . 4 |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
13		lcfrlem22.b	. . . 4 |- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
14		eqid 2451	. . . 4 |- ( LSSum ` U ) = ( LSSum ` U )
15	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	lcfrlem23 35134	. . 3 |- ( ph -> ( ( ._|_ ` { X , Y } ) ( LSSum ` U ) B ) = ( ._|_ ` { ( X .+ Y ) } ) )
16		lcfrlem24.t	. . . . . 6 |- .x. = ( .s ` U )
17		lcfrlem24.s	. . . . . 6 |- S = (Scalar ` U )
18		lcfrlem24.q	. . . . . 6 |- Q = ( 0g ` S )
19		lcfrlem24.r	. . . . . 6 |- R = ( Base ` S )
20		lcfrlem24.j	. . . . . 6 |- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
21		lcfrlem24.ib	. . . . . 6 |- ( ph -> I e. B )
22		lcfrlem24.l	. . . . . 6 |- L = (LKer ` U )
23	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22	lcfrlem24 35135	. . . . 5 |- ( ph -> ( ._|_ ` { X , Y } ) = ( ( L ` ( J ` X ) ) i^i ( L ` ( J ` Y ) ) ) )
24		inss2 3620	. . . . 5 |- ( ( L ` ( J ` X ) ) i^i ( L ` ( J ` Y ) ) ) C_ ( L ` ( J ` Y ) )
25	23, 24	syl6eqss 3449	. . . 4 |- ( ph -> ( ._|_ ` { X , Y } ) C_ ( L ` ( J ` Y ) ) )
26	1, 3, 9	dvhlvec 34678	. . . . . 6 |- ( ph -> U e. LVec )
27	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	lcfrlem22 35133	. . . . . 6 |- ( ph -> B e. A )
28		lcfrlem25.in	. . . . . 6 |- ( ph -> I =/= .0. )
29	6, 7, 8, 26, 27, 21, 28	lsatel 32572	. . . . 5 |- ( ph -> B = ( N ` { I } ) )
30		eqid 2451	. . . . . 6 |- ( LSubSp ` U ) = ( LSubSp ` U )
31	1, 3, 9	dvhlmod 34679	. . . . . 6 |- ( ph -> U e. LMod )
32		eqid 2451	. . . . . . . 8 |- (LFnl ` U ) = (LFnl ` U )
33		lcfrlem25.d	. . . . . . . 8 |- D = (LDual ` U )
34		eqid 2451	. . . . . . . 8 |- ( 0g ` D ) = ( 0g ` D )
35		eqid 2451	. . . . . . . 8 |- { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
36	1, 2, 3, 4, 5, 16, 17, 19, 6, 32, 22, 33, 34, 35, 20, 9, 11	lcfrlem10 35121	. . . . . . 7 |- ( ph -> ( J ` Y ) e. (LFnl ` U ) )
37	32, 22, 30	lkrlss 32662	. . . . . . 7 |- ( ( U e. LMod /\ ( J ` Y ) e. (LFnl ` U ) ) -> ( L ` ( J ` Y ) ) e. ( LSubSp ` U ) )
38	31, 36, 37	syl2anc 671	. . . . . 6 |- ( ph -> ( L ` ( J ` Y ) ) e. ( LSubSp ` U ) )
39		lcfrlem25.jz	. . . . . . 7 |- ( ph -> ( ( J ` Y ) ` I ) = Q )
40	4, 8, 31, 27	lsatssv 32565	. . . . . . . . 9 |- ( ph -> B C_ V )
41	40, 21	sseldd 3400	. . . . . . . 8 |- ( ph -> I e. V )
42	4, 17, 18, 32, 22, 31, 36, 41	ellkr2 32658	. . . . . . 7 |- ( ph -> ( I e. ( L ` ( J ` Y ) ) <-> ( ( J ` Y ) ` I ) = Q ) )
43	39, 42	mpbird 240	. . . . . 6 |- ( ph -> I e. ( L ` ( J ` Y ) ) )
44	30, 7, 31, 38, 43	lspsnel5a 18229	. . . . 5 |- ( ph -> ( N ` { I } ) C_ ( L ` ( J ` Y ) ) )
45	29, 44	eqsstrd 3433	. . . 4 |- ( ph -> B C_ ( L ` ( J ` Y ) ) )
46	30	lsssssubg 18191	. . . . . . 7 |- ( U e. LMod -> ( LSubSp ` U ) C_ (SubGrp ` U ) )
47	31, 46	syl 17	. . . . . 6 |- ( ph -> ( LSubSp ` U ) C_ (SubGrp ` U ) )
48	10	eldifad 3383	. . . . . . . 8 |- ( ph -> X e. V )
49	11	eldifad 3383	. . . . . . . 8 |- ( ph -> Y e. V )
50		prssi 4096	. . . . . . . 8 |- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
51	48, 49, 50	syl2anc 671	. . . . . . 7 |- ( ph -> { X , Y } C_ V )
52	1, 3, 4, 30, 2	dochlss 34923	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ { X , Y } C_ V ) -> ( ._|_ ` { X , Y } ) e. ( LSubSp ` U ) )
53	9, 51, 52	syl2anc 671	. . . . . 6 |- ( ph -> ( ._|_ ` { X , Y } ) e. ( LSubSp ` U ) )
54	47, 53	sseldd 3400	. . . . 5 |- ( ph -> ( ._|_ ` { X , Y } ) e. (SubGrp ` U ) )
55	4, 30, 7, 31, 48, 49	lspprcl 18211	. . . . . . . 8 |- ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
56	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	lcfrlem17 35128	. . . . . . . . . . 11 |- ( ph -> ( X .+ Y ) e. ( V \ { .0. } ) )
57	56	eldifad 3383	. . . . . . . . . 10 |- ( ph -> ( X .+ Y ) e. V )
58	57	snssd 4085	. . . . . . . . 9 |- ( ph -> { ( X .+ Y ) } C_ V )
59	1, 3, 4, 30, 2	dochlss 34923	. . . . . . . . 9 |- ( ( ( K e. HL /\ W e. H ) /\ { ( X .+ Y ) } C_ V ) -> ( ._|_ ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) )
60	9, 58, 59	syl2anc 671	. . . . . . . 8 |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) )
61	30	lssincl 18198	. . . . . . . 8 |- ( ( U e. LMod /\ ( N ` { X , Y } ) e. ( LSubSp ` U ) /\ ( ._|_ ` { ( X .+ Y ) } ) e. ( LSubSp ` U ) ) -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. ( LSubSp ` U ) )
62	31, 55, 60, 61	syl3anc 1271	. . . . . . 7 |- ( ph -> ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) ) e. ( LSubSp ` U ) )
63	13, 62	syl5eqel 2533	. . . . . 6 |- ( ph -> B e. ( LSubSp ` U ) )
64	47, 63	sseldd 3400	. . . . 5 |- ( ph -> B e. (SubGrp ` U ) )
65	47, 38	sseldd 3400	. . . . 5 |- ( ph -> ( L ` ( J ` Y ) ) e. (SubGrp ` U ) )
66	14	lsmlub 17325	. . . . 5 |- ( ( ( ._|_ ` { X , Y } ) e. (SubGrp ` U ) /\ B e. (SubGrp ` U ) /\ ( L ` ( J ` Y ) ) e. (SubGrp ` U ) ) -> ( ( ( ._|_ ` { X , Y } ) C_ ( L ` ( J ` Y ) ) /\ B C_ ( L ` ( J ` Y ) ) ) <-> ( ( ._|_ ` { X , Y } ) ( LSSum ` U ) B ) C_ ( L ` ( J ` Y ) ) ) )
67	54, 64, 65, 66	syl3anc 1271	. . . 4 |- ( ph -> ( ( ( ._|_ ` { X , Y } ) C_ ( L ` ( J ` Y ) ) /\ B C_ ( L ` ( J ` Y ) ) ) <-> ( ( ._|_ ` { X , Y } ) ( LSSum ` U ) B ) C_ ( L ` ( J ` Y ) ) ) )
68	25, 45, 67	mpbi2and 932	. . 3 |- ( ph -> ( ( ._|_ ` { X , Y } ) ( LSSum ` U ) B ) C_ ( L ` ( J ` Y ) ) )
69	15, 68	eqsstr3d 3434	. 2 |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) C_ ( L ` ( J ` Y ) ) )
70		eqid 2451	. . 3 |- (LSHyp ` U ) = (LSHyp ` U )
71	1, 2, 3, 4, 6, 70, 9, 56	dochsnshp 35022	. . 3 |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) e. (LSHyp ` U ) )
72	1, 2, 3, 4, 5, 16, 17, 19, 6, 32, 22, 33, 34, 35, 20, 9, 11	lcfrlem13 35124	. . . . 5 |- ( ph -> ( J ` Y ) e. ( { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } \ { ( 0g ` D ) } ) )
73		eldifsni 4066	. . . . 5 |- ( ( J ` Y ) e. ( { f e. (LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } \ { ( 0g ` D ) } ) -> ( J ` Y ) =/= ( 0g ` D ) )
74	72, 73	syl 17	. . . 4 |- ( ph -> ( J ` Y ) =/= ( 0g ` D ) )
75	70, 32, 22, 33, 34, 26, 36	lduallkr3 32729	. . . 4 |- ( ph -> ( ( L ` ( J ` Y ) ) e. (LSHyp ` U ) <-> ( J ` Y ) =/= ( 0g ` D ) ) )
76	74, 75	mpbird 240	. . 3 |- ( ph -> ( L ` ( J ` Y ) ) e. (LSHyp ` U ) )
77	70, 26, 71, 76	lshpcmp 32555	. 2 |- ( ph -> ( ( ._|_ ` { ( X .+ Y ) } ) C_ ( L ` ( J ` Y ) ) <-> ( ._|_ ` { ( X .+ Y ) } ) = ( L ` ( J ` Y ) ) ) )
78	69, 77	mpbid 215	1 |- ( ph -> ( ._|_ ` { ( X .+ Y ) } ) = ( L ` ( J ` Y ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1447   e. wcel 1890   =/= wne 2621   E.wrex 2737   {crab 2740   \ cdif 3368   i^i cin 3370   C_ wss 3371   {csn 3935   {cpr 3937   |-> cmpt 4432   ` cfv 5560   iota_crio 6236  (class class class)co 6275   Basecbs 15131   +g cplusg 15200  Scalarcsca 15203   .scvsca 15204   0gc0g 15348  SubGrpcsubg 16821   LSSumclsm 17296   LModclmod 18101   LSubSpclss 18165   LSpanclspn 18204  LSAtomsclsa 32541  LSHypclsh 32542  LFnlclfn 32624  LKerclk 32652  LDualcld 32690   HLchlt 32917   LHypclh 33550   DVecHcdvh 34647   ocHcoch 34916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602  ax-riotaBAD 32526

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-fal 1453  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-iun 4249  df-iin 4250  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-of 6518  df-om 6680  df-1st 6780  df-2nd 6781  df-tpos 6959  df-undef 7006  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-1o 7168  df-oadd 7172  df-er 7349  df-map 7460  df-en 7556  df-dom 7557  df-sdom 7558  df-fin 7559  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-nn 10598  df-2 10656  df-3 10657  df-4 10658  df-5 10659  df-6 10660  df-n0 10859  df-z 10927  df-uz 11149  df-fz 11775  df-struct 15133  df-ndx 15134  df-slot 15135  df-base 15136  df-sets 15137  df-ress 15138  df-plusg 15213  df-mulr 15214  df-sca 15216  df-vsca 15217  df-0g 15350  df-mre 15502  df-mrc 15503  df-acs 15505  df-preset 16183  df-poset 16201  df-plt 16214  df-lub 16230  df-glb 16231  df-join 16232  df-meet 16233  df-p0 16295  df-p1 16296  df-lat 16302  df-clat 16364  df-mgm 16498  df-sgrp 16537  df-mnd 16547  df-submnd 16593  df-grp 16683  df-minusg 16684  df-sbg 16685  df-subg 16824  df-cntz 16981  df-oppg 17007  df-lsm 17298  df-cmn 17442  df-abl 17443  df-mgp 17734  df-ur 17746  df-ring 17792  df-oppr 17861  df-dvdsr 17879  df-unit 17880  df-invr 17910  df-dvr 17921  df-drng 17987  df-lmod 18103  df-lss 18166  df-lsp 18205  df-lvec 18336  df-lsatoms 32543  df-lshyp 32544  df-lcv 32586  df-lfl 32625  df-lkr 32653  df-ldual 32691  df-oposet 32743  df-ol 32745  df-oml 32746  df-covers 32833  df-ats 32834  df-atl 32865  df-cvlat 32889  df-hlat 32918  df-llines 33064  df-lplanes 33065  df-lvols 33066  df-lines 33067  df-psubsp 33069  df-pmap 33070  df-padd 33362  df-lhyp 33554  df-laut 33555  df-ldil 33670  df-ltrn 33671  df-trl 33726  df-tgrp 34311  df-tendo 34323  df-edring 34325  df-dveca 34571  df-disoa 34598  df-dvech 34648  df-dib 34708  df-dic 34742  df-dih 34798  df-doch 34917  df-djh 34964

This theorem is referenced by:  lcfrlem26  35137