This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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