Theorem islindf 20151

Description: Property of an independent family of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015.)

Hypotheses

Ref	Expression
islindf.b	|- B = ( Base ` W )
islindf.v	|- .x. = ( .s ` W )
islindf.k	|- K = ( LSpan ` W )
islindf.s	|- S = (Scalar ` W )
islindf.n	|- N = ( Base ` S )
islindf.z	|- .0. = ( 0g ` S )

Assertion

Ref	Expression
islindf	|- ( ( W e. Y /\ F e. X ) -> ( F LIndF W <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )

Distinct variable groups:   k, F, x   k, N   k, W, x   .0. , k

Allowed substitution hints:   B( x, k)   S( x, k)   .x. ( x, k)   K( x, k)   N( x)   X( x, k)   Y( x, k)   .0. ( x)

Proof of Theorem islindf

Dummy variables f w s are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		feq1 6026	. . . . . 6 |- ( f = F -> ( f : dom f --> ( Base ` w ) <-> F : dom f --> ( Base ` w ) ) )
2	1	adantr 481	. . . . 5 |- ( ( f = F /\ w = W ) -> ( f : dom f --> ( Base ` w ) <-> F : dom f --> ( Base ` w ) ) )
3		dmeq 5324	. . . . . . 7 |- ( f = F -> dom f = dom F )
4	3	adantr 481	. . . . . 6 |- ( ( f = F /\ w = W ) -> dom f = dom F )
5		fveq2 6191	. . . . . . . 8 |- ( w = W -> ( Base ` w ) = ( Base ` W ) )
6		islindf.b	. . . . . . . 8 |- B = ( Base ` W )
7	5, 6	syl6eqr 2674	. . . . . . 7 |- ( w = W -> ( Base ` w ) = B )
8	7	adantl 482	. . . . . 6 |- ( ( f = F /\ w = W ) -> ( Base ` w ) = B )
9	4, 8	feq23d 6040	. . . . 5 |- ( ( f = F /\ w = W ) -> ( F : dom f --> ( Base ` w ) <-> F : dom F --> B ) )
10	2, 9	bitrd 268	. . . 4 |- ( ( f = F /\ w = W ) -> ( f : dom f --> ( Base ` w ) <-> F : dom F --> B ) )
11		fvex 6201	. . . . . 6 |- (Scalar ` w ) e. _V
12		fveq2 6191	. . . . . . . . 9 |- ( s = (Scalar ` w ) -> ( Base ` s ) = ( Base ` (Scalar ` w ) ) )
13		fveq2 6191	. . . . . . . . . 10 |- ( s = (Scalar ` w ) -> ( 0g ` s ) = ( 0g ` (Scalar ` w ) ) )
14	13	sneqd 4189	. . . . . . . . 9 |- ( s = (Scalar ` w ) -> { ( 0g ` s ) } = { ( 0g ` (Scalar ` w ) ) } )
15	12, 14	difeq12d 3729	. . . . . . . 8 |- ( s = (Scalar ` w ) -> ( ( Base ` s ) \ { ( 0g ` s ) } ) = ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) )
16	15	raleqdv 3144	. . . . . . 7 |- ( s = (Scalar ` w ) -> ( A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. k e. ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) )
17	16	ralbidv 2986	. . . . . 6 |- ( s = (Scalar ` w ) -> ( A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom f A. k e. ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) )
18	11, 17	sbcie 3470	. . . . 5 |- ( [. (Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom f A. k e. ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) )
19		fveq2 6191	. . . . . . . . . . . 12 |- ( w = W -> (Scalar ` w ) = (Scalar ` W ) )
20		islindf.s	. . . . . . . . . . . 12 |- S = (Scalar ` W )
21	19, 20	syl6eqr 2674	. . . . . . . . . . 11 |- ( w = W -> (Scalar ` w ) = S )
22	21	fveq2d 6195	. . . . . . . . . 10 |- ( w = W -> ( Base ` (Scalar ` w ) ) = ( Base ` S ) )
23		islindf.n	. . . . . . . . . 10 |- N = ( Base ` S )
24	22, 23	syl6eqr 2674	. . . . . . . . 9 |- ( w = W -> ( Base ` (Scalar ` w ) ) = N )
25	21	fveq2d 6195	. . . . . . . . . . 11 |- ( w = W -> ( 0g ` (Scalar ` w ) ) = ( 0g ` S ) )
26		islindf.z	. . . . . . . . . . 11 |- .0. = ( 0g ` S )
27	25, 26	syl6eqr 2674	. . . . . . . . . 10 |- ( w = W -> ( 0g ` (Scalar ` w ) ) = .0. )
28	27	sneqd 4189	. . . . . . . . 9 |- ( w = W -> { ( 0g ` (Scalar ` w ) ) } = { .0. } )
29	24, 28	difeq12d 3729	. . . . . . . 8 |- ( w = W -> ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) = ( N \ { .0. } ) )
30	29	adantl 482	. . . . . . 7 |- ( ( f = F /\ w = W ) -> ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) = ( N \ { .0. } ) )
31		fveq2 6191	. . . . . . . . . . . 12 |- ( w = W -> ( .s ` w ) = ( .s ` W ) )
32		islindf.v	. . . . . . . . . . . 12 |- .x. = ( .s ` W )
33	31, 32	syl6eqr 2674	. . . . . . . . . . 11 |- ( w = W -> ( .s ` w ) = .x. )
34	33	adantl 482	. . . . . . . . . 10 |- ( ( f = F /\ w = W ) -> ( .s ` w ) = .x. )
35		eqidd 2623	. . . . . . . . . 10 |- ( ( f = F /\ w = W ) -> k = k )
36		fveq1 6190	. . . . . . . . . . 11 |- ( f = F -> ( f ` x ) = ( F ` x ) )
37	36	adantr 481	. . . . . . . . . 10 |- ( ( f = F /\ w = W ) -> ( f ` x ) = ( F ` x ) )
38	34, 35, 37	oveq123d 6671	. . . . . . . . 9 |- ( ( f = F /\ w = W ) -> ( k ( .s ` w ) ( f ` x ) ) = ( k .x. ( F ` x ) ) )
39		fveq2 6191	. . . . . . . . . . . 12 |- ( w = W -> ( LSpan ` w ) = ( LSpan ` W ) )
40		islindf.k	. . . . . . . . . . . 12 |- K = ( LSpan ` W )
41	39, 40	syl6eqr 2674	. . . . . . . . . . 11 |- ( w = W -> ( LSpan ` w ) = K )
42	41	adantl 482	. . . . . . . . . 10 |- ( ( f = F /\ w = W ) -> ( LSpan ` w ) = K )
43		imaeq1 5461	. . . . . . . . . . . 12 |- ( f = F -> ( f " ( dom f \ { x } ) ) = ( F " ( dom f \ { x } ) ) )
44	3	difeq1d 3727	. . . . . . . . . . . . 13 |- ( f = F -> ( dom f \ { x } ) = ( dom F \ { x } ) )
45	44	imaeq2d 5466	. . . . . . . . . . . 12 |- ( f = F -> ( F " ( dom f \ { x } ) ) = ( F " ( dom F \ { x } ) ) )
46	43, 45	eqtrd 2656	. . . . . . . . . . 11 |- ( f = F -> ( f " ( dom f \ { x } ) ) = ( F " ( dom F \ { x } ) ) )
47	46	adantr 481	. . . . . . . . . 10 |- ( ( f = F /\ w = W ) -> ( f " ( dom f \ { x } ) ) = ( F " ( dom F \ { x } ) ) )
48	42, 47	fveq12d 6197	. . . . . . . . 9 |- ( ( f = F /\ w = W ) -> ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) = ( K ` ( F " ( dom F \ { x } ) ) ) )
49	38, 48	eleq12d 2695	. . . . . . . 8 |- ( ( f = F /\ w = W ) -> ( ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
50	49	notbid 308	. . . . . . 7 |- ( ( f = F /\ w = W ) -> ( -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
51	30, 50	raleqbidv 3152	. . . . . 6 |- ( ( f = F /\ w = W ) -> ( A. k e. ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
52	4, 51	raleqbidv 3152	. . . . 5 |- ( ( f = F /\ w = W ) -> ( A. x e. dom f A. k e. ( ( Base ` (Scalar ` w ) ) \ { ( 0g ` (Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
53	18, 52	syl5bb 272	. . . 4 |- ( ( f = F /\ w = W ) -> ( [. (Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
54	10, 53	anbi12d 747	. . 3 |- ( ( f = F /\ w = W ) -> ( ( f : dom f --> ( Base ` w ) /\ [. (Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )
55		df-lindf 20145	. . 3 |- LIndF = { <. f , w >. | ( f : dom f --> ( Base ` w ) /\ [. (Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) }
56	54, 55	brabga 4989	. 2 |- ( ( F e. X /\ W e. Y ) -> ( F LIndF W <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )
57	56	ancoms 469	1 |- ( ( W e. Y /\ F e. X ) -> ( F LIndF W <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   [.wsbc 3435   \ cdif 3571   {csn 4177   class class class wbr 4653   dom cdm 5114   "cima 5117   -->wf 5884   ` cfv 5888  (class class class)co 6650   Basecbs 15857  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   LSpanclspn 18971   LIndF clindf 20143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-lindf 20145

This theorem is referenced by:  islinds2  20152  islindf2  20153  lindff  20154  lindfind  20155  f1lindf  20161  lsslindf  20169  matunitlindf  33407