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=RfreeLModI
islindf5.b B=BaseF
islindf5.c C=BaseT
islindf5.v ·˙=T
islindf5.e E=xBTx·˙fA
islindf5.t φTLMod
islindf5.i φIX
islindf5.r φR=ScalarT
islindf5.a φA:IC
Assertion islindf5 φALIndFTE:B1-1C

Proof

Step Hyp Ref Expression
1 islindf5.f F=RfreeLModI
2 islindf5.b B=BaseF
3 islindf5.c C=BaseT
4 islindf5.v ·˙=T
5 islindf5.e E=xBTx·˙fA
6 islindf5.t φTLMod
7 islindf5.i φIX
8 islindf5.r φR=ScalarT
9 islindf5.a φA:IC
10 eqid ScalarT=ScalarT
11 eqid 0T=0T
12 eqid 0ScalarT=0ScalarT
13 eqid BaseScalarTfreeLModI=BaseScalarTfreeLModI
14 3 10 4 11 12 13 islindf4 TLModIXA:ICALIndFTyBaseScalarTfreeLModITy·˙fA=0Ty=I×0ScalarT
15 6 7 9 14 syl3anc φALIndFTyBaseScalarTfreeLModITy·˙fA=0Ty=I×0ScalarT
16 oveq1 x=yx·˙fA=y·˙fA
17 16 oveq2d x=yTx·˙fA=Ty·˙fA
18 ovex Ty·˙fAV
19 17 5 18 fvmpt yBEy=Ty·˙fA
20 19 adantl φyBEy=Ty·˙fA
21 20 eqeq1d φyBEy=0TTy·˙fA=0T
22 10 lmodring TLModScalarTRing
23 6 22 syl φScalarTRing
24 8 23 eqeltrd φRRing
25 eqid 0R=0R
26 1 25 frlm0 RRingIXI×0R=0F
27 24 7 26 syl2anc φI×0R=0F
28 8 fveq2d φ0R=0ScalarT
29 28 sneqd φ0R=0ScalarT
30 29 xpeq2d φI×0R=I×0ScalarT
31 27 30 eqtr3d φ0F=I×0ScalarT
32 31 adantr φyB0F=I×0ScalarT
33 32 eqeq2d φyBy=0Fy=I×0ScalarT
34 21 33 imbi12d φyBEy=0Ty=0FTy·˙fA=0Ty=I×0ScalarT
35 34 ralbidva φyBEy=0Ty=0FyBTy·˙fA=0Ty=I×0ScalarT
36 8 eqcomd φScalarT=R
37 36 oveq1d φScalarTfreeLModI=RfreeLModI
38 37 1 eqtr4di φScalarTfreeLModI=F
39 38 fveq2d φBaseScalarTfreeLModI=BaseF
40 39 2 eqtr4di φBaseScalarTfreeLModI=B
41 40 raleqdv φyBaseScalarTfreeLModITy·˙fA=0Ty=I×0ScalarTyBTy·˙fA=0Ty=I×0ScalarT
42 35 41 bitr4d φyBEy=0Ty=0FyBaseScalarTfreeLModITy·˙fA=0Ty=I×0ScalarT
43 15 42 bitr4d φALIndFTyBEy=0Ty=0F
44 1 2 3 4 5 6 7 8 9 frlmup1 φEFLMHomT
45 lmghm EFLMHomTEFGrpHomT
46 eqid 0F=0F
47 2 3 46 11 ghmf1 EFGrpHomTE:B1-1CyBEy=0Ty=0F
48 44 45 47 3syl φE:B1-1CyBEy=0Ty=0F
49 43 48 bitr4d φALIndFTE:B1-1C