Metamath Proof Explorer

Theorem lindfmm

Description: Linear independence of a family is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses lindfmm.b ⊢B=BaseS
lindfmm.c ⊢C=BaseT
Assertion lindfmm ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→FLIndFS↔G∘FLIndFT

Proof

Step Hyp Ref Expression
1 lindfmm.b ⊢B=BaseS
2 lindfmm.c ⊢C=BaseT
3 rellindf ⊢Rel⁡LIndF
4 3 brrelex1i ⊢FLIndFS→F∈V
5 simp3 ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→F:I⟶B
6 dmfex ⊢F∈V∧F:I⟶B→I∈V
7 4 5 6 syl2anr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧FLIndFS→I∈V
8 7 ex ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→FLIndFS→I∈V
9 3 brrelex1i ⊢G∘FLIndFT→G∘F∈V
10 f1f ⊢G:B⟶1-1C→G:B⟶C
11 fco ⊢G:B⟶C∧F:I⟶B→G∘F:I⟶C
12 10 11 sylan ⊢G:B⟶1-1C∧F:I⟶B→G∘F:I⟶C
13 12 3adant1 ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→G∘F:I⟶C
14 dmfex ⊢G∘F∈V∧G∘F:I⟶C→I∈V
15 9 13 14 syl2anr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧G∘FLIndFT→I∈V
16 15 ex ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→G∘FLIndFT→I∈V
17 eldifi ⊢k∈BaseScalar⁡S∖0Scalar⁡S→k∈BaseScalar⁡S
18 simpllr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G:B⟶1-1C
19 lmhmlmod1 ⊢G∈SLMHomT→S∈LMod
20 19 ad3antrrr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→S∈LMod
21 simprr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→k∈BaseScalar⁡S
22 simprl ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→F:I⟶B
23 simpl ⊢x∈I∧k∈BaseScalar⁡S→x∈I
24 ffvelcdm ⊢F:I⟶B∧x∈I→F⁡x∈B
25 22 23 24 syl2an ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→F⁡x∈B
26 eqid ⊢Scalar⁡S=Scalar⁡S
27 eqid ⊢⋅S=⋅S
28 eqid ⊢BaseScalar⁡S=BaseScalar⁡S
29 1 26 27 28 lmodvscl ⊢S∈LMod∧k∈BaseScalar⁡S∧F⁡x∈B→k⋅SF⁡x∈B
30 20 21 25 29 syl3anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→k⋅SF⁡x∈B
31 imassrn ⊢FI∖x⊆ran⁡F
32 frn ⊢F:I⟶B→ran⁡F⊆B
33 32 adantr ⊢F:I⟶B∧I∈V→ran⁡F⊆B
34 31 33 sstrid ⊢F:I⟶B∧I∈V→FI∖x⊆B
35 34 ad2antlr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→FI∖x⊆B
36 eqid ⊢LSpan⁡S=LSpan⁡S
37 1 36 lspssv ⊢S∈LMod∧FI∖x⊆B→LSpan⁡S⁡FI∖x⊆B
38 20 35 37 syl2anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→LSpan⁡S⁡FI∖x⊆B
39 f1elima ⊢G:B⟶1-1C∧k⋅SF⁡x∈B∧LSpan⁡S⁡FI∖x⊆B→G⁡k⋅SF⁡x∈GLSpan⁡S⁡FI∖x↔k⋅SF⁡x∈LSpan⁡S⁡FI∖x
40 18 30 38 39 syl3anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G⁡k⋅SF⁡x∈GLSpan⁡S⁡FI∖x↔k⋅SF⁡x∈LSpan⁡S⁡FI∖x
41 simplll ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G∈SLMHomT
42 eqid ⊢⋅T=⋅T
43 26 28 1 27 42 lmhmlin ⊢G∈SLMHomT∧k∈BaseScalar⁡S∧F⁡x∈B→G⁡k⋅SF⁡x=k⋅TG⁡F⁡x
44 41 21 25 43 syl3anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G⁡k⋅SF⁡x=k⋅TG⁡F⁡x
45 ffn ⊢F:I⟶B→FFnI
46 45 ad2antrl ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→FFnI
47 fvco2 ⊢FFnI∧x∈I→G∘F⁡x=G⁡F⁡x
48 46 23 47 syl2an ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G∘F⁡x=G⁡F⁡x
49 48 oveq2d ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→k⋅TG∘F⁡x=k⋅TG⁡F⁡x
50 44 49 eqtr4d ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G⁡k⋅SF⁡x=k⋅TG∘F⁡x
51 eqid ⊢LSpan⁡T=LSpan⁡T
52 1 36 51 lmhmlsp ⊢G∈SLMHomT∧FI∖x⊆B→GLSpan⁡S⁡FI∖x=LSpan⁡T⁡GFI∖x
53 41 35 52 syl2anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→GLSpan⁡S⁡FI∖x=LSpan⁡T⁡GFI∖x
54 imaco ⊢G∘FI∖x=GFI∖x
55 54 fveq2i ⊢LSpan⁡T⁡G∘FI∖x=LSpan⁡T⁡GFI∖x
56 53 55 eqtr4di ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→GLSpan⁡S⁡FI∖x=LSpan⁡T⁡G∘FI∖x
57 50 56 eleq12d ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→G⁡k⋅SF⁡x∈GLSpan⁡S⁡FI∖x↔k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
58 40 57 bitr3d ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
59 58 notbid ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
60 59 anassrs ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S→¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
61 17 60 sylan2 ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I∧k∈BaseScalar⁡S∖0Scalar⁡S→¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
62 61 ralbidva ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I→∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
63 eqid ⊢Scalar⁡T=Scalar⁡T
64 26 63 lmhmsca ⊢G∈SLMHomT→Scalar⁡T=Scalar⁡S
65 64 fveq2d ⊢G∈SLMHomT→BaseScalar⁡T=BaseScalar⁡S
66 64 fveq2d ⊢G∈SLMHomT→0Scalar⁡T=0Scalar⁡S
67 66 sneqd ⊢G∈SLMHomT→0Scalar⁡T=0Scalar⁡S
68 65 67 difeq12d ⊢G∈SLMHomT→BaseScalar⁡T∖0Scalar⁡T=BaseScalar⁡S∖0Scalar⁡S
69 68 ad3antrrr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I→BaseScalar⁡T∖0Scalar⁡T=BaseScalar⁡S∖0Scalar⁡S
70 69 raleqdv ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I→∀k∈BaseScalar⁡T∖0Scalar⁡T¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x↔∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
71 62 70 bitr4d ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V∧x∈I→∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔∀k∈BaseScalar⁡T∖0Scalar⁡T¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
72 71 ralbidva ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→∀x∈I∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x↔∀x∈I∀k∈BaseScalar⁡T∖0Scalar⁡T¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
73 19 ad2antrr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→S∈LMod
74 simprr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→I∈V
75 eqid ⊢0Scalar⁡S=0Scalar⁡S
76 1 27 36 26 28 75 islindf2 ⊢S∈LMod∧I∈V∧F:I⟶B→FLIndFS↔∀x∈I∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x
77 73 74 22 76 syl3anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→FLIndFS↔∀x∈I∀k∈BaseScalar⁡S∖0Scalar⁡S¬k⋅SF⁡x∈LSpan⁡S⁡FI∖x
78 lmhmlmod2 ⊢G∈SLMHomT→T∈LMod
79 78 ad2antrr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→T∈LMod
80 12 ad2ant2lr ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→G∘F:I⟶C
81 eqid ⊢BaseScalar⁡T=BaseScalar⁡T
82 eqid ⊢0Scalar⁡T=0Scalar⁡T
83 2 42 51 63 81 82 islindf2 ⊢T∈LMod∧I∈V∧G∘F:I⟶C→G∘FLIndFT↔∀x∈I∀k∈BaseScalar⁡T∖0Scalar⁡T¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
84 79 74 80 83 syl3anc ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→G∘FLIndFT↔∀x∈I∀k∈BaseScalar⁡T∖0Scalar⁡T¬k⋅TG∘F⁡x∈LSpan⁡T⁡G∘FI∖x
85 72 77 84 3bitr4d ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B∧I∈V→FLIndFS↔G∘FLIndFT
86 85 exp32 ⊢G∈SLMHomT∧G:B⟶1-1C→F:I⟶B→I∈V→FLIndFS↔G∘FLIndFT
87 86 3impia ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→I∈V→FLIndFS↔G∘FLIndFT
88 8 16 87 pm5.21ndd ⊢G∈SLMHomT∧G:B⟶1-1C∧F:I⟶B→FLIndFS↔G∘FLIndFT