Metamath Proof Explorer


Theorem islindf2

Description: Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses islindf.b B = Base W
islindf.v · ˙ = W
islindf.k K = LSpan W
islindf.s S = Scalar W
islindf.n N = Base S
islindf.z 0 ˙ = 0 S
Assertion islindf2 W Y I X F : I B F LIndF W x I k N 0 ˙ ¬ k · ˙ F x K F I x

Proof

Step Hyp Ref Expression
1 islindf.b B = Base W
2 islindf.v · ˙ = W
3 islindf.k K = LSpan W
4 islindf.s S = Scalar W
5 islindf.n N = Base S
6 islindf.z 0 ˙ = 0 S
7 simp1 W Y I X F : I B W Y
8 simp3 W Y I X F : I B F : I B
9 simp2 W Y I X F : I B I X
10 8 9 fexd W Y I X F : I B F V
11 1 2 3 4 5 6 islindf W Y F V F LIndF W F : dom F B x dom F k N 0 ˙ ¬ k · ˙ F x K F dom F x
12 7 10 11 syl2anc W Y I X F : I B F LIndF W F : dom F B x dom F k N 0 ˙ ¬ k · ˙ F x K F dom F x
13 ffdm F : I B F : dom F B dom F I
14 13 simpld F : I B F : dom F B
15 14 3ad2ant3 W Y I X F : I B F : dom F B
16 15 biantrurd W Y I X F : I B x dom F k N 0 ˙ ¬ k · ˙ F x K F dom F x F : dom F B x dom F k N 0 ˙ ¬ k · ˙ F x K F dom F x
17 fdm F : I B dom F = I
18 17 3ad2ant3 W Y I X F : I B dom F = I
19 18 difeq1d W Y I X F : I B dom F x = I x
20 19 imaeq2d W Y I X F : I B F dom F x = F I x
21 20 fveq2d W Y I X F : I B K F dom F x = K F I x
22 21 eleq2d W Y I X F : I B k · ˙ F x K F dom F x k · ˙ F x K F I x
23 22 notbid W Y I X F : I B ¬ k · ˙ F x K F dom F x ¬ k · ˙ F x K F I x
24 23 ralbidv W Y I X F : I B k N 0 ˙ ¬ k · ˙ F x K F dom F x k N 0 ˙ ¬ k · ˙ F x K F I x
25 18 24 raleqbidv W Y I X F : I B x dom F k N 0 ˙ ¬ k · ˙ F x K F dom F x x I k N 0 ˙ ¬ k · ˙ F x K F I x
26 12 16 25 3bitr2d W Y I X F : I B F LIndF W x I k N 0 ˙ ¬ k · ˙ F x K F I x