Metamath Proof Explorer

Theorem islindf5

Description: A family is independent iff the linear combinations homomorphism is injective. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses islindf5.f 
|- F = ( R freeLMod I )
islindf5.b 
|- B = ( Base ` F )
islindf5.c 
|- C = ( Base ` T )
islindf5.v 
|- .x. = ( .s ` T )
islindf5.e 
|- E = ( x e. B |-> ( T gsum ( x oF .x. A ) ) )
islindf5.t 
|- ( ph -> T e. LMod )
islindf5.i 
|- ( ph -> I e. X )
islindf5.r 
|- ( ph -> R = ( Scalar ` T ) )
islindf5.a 
|- ( ph -> A : I --> C )
Assertion islindf5 
|- ( ph -> ( A LIndF T <-> E : B -1-1-> C ) )

Proof

Step Hyp Ref Expression
1 islindf5.f 
 |-  F = ( R freeLMod I )
2 islindf5.b 
 |-  B = ( Base ` F )
3 islindf5.c 
 |-  C = ( Base ` T )
4 islindf5.v 
 |-  .x. = ( .s ` T )
5 islindf5.e 
 |-  E = ( x e. B |-> ( T gsum ( x oF .x. A ) ) )
6 islindf5.t 
 |-  ( ph -> T e. LMod )
7 islindf5.i 
 |-  ( ph -> I e. X )
8 islindf5.r 
 |-  ( ph -> R = ( Scalar ` T ) )
9 islindf5.a 
 |-  ( ph -> A : I --> C )
10 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
11 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
12 eqid 
 |-  ( 0g ` ( Scalar ` T ) ) = ( 0g ` ( Scalar ` T ) )
13 eqid 
 |-  ( Base ` ( ( Scalar ` T ) freeLMod I ) ) = ( Base ` ( ( Scalar ` T ) freeLMod I ) )
14 3 10 4 11 12 13 islindf4 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ( A LIndF T <-> A. y e. ( Base ` ( ( Scalar ` T ) freeLMod I ) ) ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) ) )
15 6 7 9 14 syl3anc 
 |-  ( ph -> ( A LIndF T <-> A. y e. ( Base ` ( ( Scalar ` T ) freeLMod I ) ) ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) ) )
16 oveq1 
 |-  ( x = y -> ( x oF .x. A ) = ( y oF .x. A ) )
17 16 oveq2d 
 |-  ( x = y -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( y oF .x. A ) ) )
18 ovex 
 |-  ( T gsum ( y oF .x. A ) ) e. _V
19 17 5 18 fvmpt 
 |-  ( y e. B -> ( E ` y ) = ( T gsum ( y oF .x. A ) ) )
20 19 adantl 
 |-  ( ( ph /\ y e. B ) -> ( E ` y ) = ( T gsum ( y oF .x. A ) ) )
21 20 eqeq1d 
 |-  ( ( ph /\ y e. B ) -> ( ( E ` y ) = ( 0g ` T ) <-> ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) ) )
22 10 lmodring 
 |-  ( T e. LMod -> ( Scalar ` T ) e. Ring )
23 6 22 syl 
 |-  ( ph -> ( Scalar ` T ) e. Ring )
24 8 23 eqeltrd 
 |-  ( ph -> R e. Ring )
25 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
26 1 25 frlm0 
 |-  ( ( R e. Ring /\ I e. X ) -> ( I X. { ( 0g ` R ) } ) = ( 0g ` F ) )
27 24 7 26 syl2anc 
 |-  ( ph -> ( I X. { ( 0g ` R ) } ) = ( 0g ` F ) )
28 8 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` T ) ) )
29 28 sneqd 
 |-  ( ph -> { ( 0g ` R ) } = { ( 0g ` ( Scalar ` T ) ) } )
30 29 xpeq2d 
 |-  ( ph -> ( I X. { ( 0g ` R ) } ) = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) )
31 27 30 eqtr3d 
 |-  ( ph -> ( 0g ` F ) = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) )
32 31 adantr 
 |-  ( ( ph /\ y e. B ) -> ( 0g ` F ) = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) )
33 32 eqeq2d 
 |-  ( ( ph /\ y e. B ) -> ( y = ( 0g ` F ) <-> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) )
34 21 33 imbi12d 
 |-  ( ( ph /\ y e. B ) -> ( ( ( E ` y ) = ( 0g ` T ) -> y = ( 0g ` F ) ) <-> ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) ) )
35 34 ralbidva 
 |-  ( ph -> ( A. y e. B ( ( E ` y ) = ( 0g ` T ) -> y = ( 0g ` F ) ) <-> A. y e. B ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) ) )
36 8 eqcomd 
 |-  ( ph -> ( Scalar ` T ) = R )
37 36 oveq1d 
 |-  ( ph -> ( ( Scalar ` T ) freeLMod I ) = ( R freeLMod I ) )
38 37 1 eqtr4di 
 |-  ( ph -> ( ( Scalar ` T ) freeLMod I ) = F )
39 38 fveq2d 
 |-  ( ph -> ( Base ` ( ( Scalar ` T ) freeLMod I ) ) = ( Base ` F ) )
40 39 2 eqtr4di 
 |-  ( ph -> ( Base ` ( ( Scalar ` T ) freeLMod I ) ) = B )
41 40 raleqdv 
 |-  ( ph -> ( A. y e. ( Base ` ( ( Scalar ` T ) freeLMod I ) ) ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) <-> A. y e. B ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) ) )
42 35 41 bitr4d 
 |-  ( ph -> ( A. y e. B ( ( E ` y ) = ( 0g ` T ) -> y = ( 0g ` F ) ) <-> A. y e. ( Base ` ( ( Scalar ` T ) freeLMod I ) ) ( ( T gsum ( y oF .x. A ) ) = ( 0g ` T ) -> y = ( I X. { ( 0g ` ( Scalar ` T ) ) } ) ) ) )
43 15 42 bitr4d 
 |-  ( ph -> ( A LIndF T <-> A. y e. B ( ( E ` y ) = ( 0g ` T ) -> y = ( 0g ` F ) ) ) )
44 1 2 3 4 5 6 7 8 9 frlmup1 
 |-  ( ph -> E e. ( F LMHom T ) )
45 lmghm 
 |-  ( E e. ( F LMHom T ) -> E e. ( F GrpHom T ) )
46 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
47 2 3 46 11 ghmf1 
 |-  ( E e. ( F GrpHom T ) -> ( E : B -1-1-> C <-> A. y e. B ( ( E ` y ) = ( 0g ` T ) -> y = ( 0g ` F ) ) ) )
48 44 45 47 3syl 
 |-  ( ph -> ( E : B -1-1-> C <-> A. y e. B ( ( E ` y ) = ( 0g ` T ) -> y = ( 0g ` F ) ) ) )
49 43 48 bitr4d 
 |-  ( ph -> ( A LIndF T <-> E : B -1-1-> C ) )