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 = Base S
lindfmm.c C = Base T
Assertion lindfmm G S LMHom T G : B 1-1 C F : I B F LIndF S G F LIndF T

Proof

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