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 𝐹 = ( 𝑅 freeLMod 𝐼 )
islindf5.b 𝐵 = ( Base ‘ 𝐹 )
islindf5.c 𝐶 = ( Base ‘ 𝑇 )
islindf5.v · = ( ·𝑠𝑇 )
islindf5.e 𝐸 = ( 𝑥𝐵 ↦ ( 𝑇 Σg ( 𝑥f · 𝐴 ) ) )
islindf5.t ( 𝜑𝑇 ∈ LMod )
islindf5.i ( 𝜑𝐼𝑋 )
islindf5.r ( 𝜑𝑅 = ( Scalar ‘ 𝑇 ) )
islindf5.a ( 𝜑𝐴 : 𝐼𝐶 )
Assertion islindf5 ( 𝜑 → ( 𝐴 LIndF 𝑇𝐸 : 𝐵1-1𝐶 ) )

Proof

Step Hyp Ref Expression
1 islindf5.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 islindf5.b 𝐵 = ( Base ‘ 𝐹 )
3 islindf5.c 𝐶 = ( Base ‘ 𝑇 )
4 islindf5.v · = ( ·𝑠𝑇 )
5 islindf5.e 𝐸 = ( 𝑥𝐵 ↦ ( 𝑇 Σg ( 𝑥f · 𝐴 ) ) )
6 islindf5.t ( 𝜑𝑇 ∈ LMod )
7 islindf5.i ( 𝜑𝐼𝑋 )
8 islindf5.r ( 𝜑𝑅 = ( Scalar ‘ 𝑇 ) )
9 islindf5.a ( 𝜑𝐴 : 𝐼𝐶 )
10 eqid ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
11 eqid ( 0g𝑇 ) = ( 0g𝑇 )
12 eqid ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) )
13 eqid ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) = ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) )
14 3 10 4 11 12 13 islindf4 ( ( 𝑇 ∈ LMod ∧ 𝐼𝑋𝐴 : 𝐼𝐶 ) → ( 𝐴 LIndF 𝑇 ↔ ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) )
15 6 7 9 14 syl3anc ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) )
16 oveq1 ( 𝑥 = 𝑦 → ( 𝑥f · 𝐴 ) = ( 𝑦f · 𝐴 ) )
17 16 oveq2d ( 𝑥 = 𝑦 → ( 𝑇 Σg ( 𝑥f · 𝐴 ) ) = ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) )
18 ovex ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) ∈ V
19 17 5 18 fvmpt ( 𝑦𝐵 → ( 𝐸𝑦 ) = ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) )
20 19 adantl ( ( 𝜑𝑦𝐵 ) → ( 𝐸𝑦 ) = ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) )
21 20 eqeq1d ( ( 𝜑𝑦𝐵 ) → ( ( 𝐸𝑦 ) = ( 0g𝑇 ) ↔ ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) ) )
22 10 lmodring ( 𝑇 ∈ LMod → ( Scalar ‘ 𝑇 ) ∈ Ring )
23 6 22 syl ( 𝜑 → ( Scalar ‘ 𝑇 ) ∈ Ring )
24 8 23 eqeltrd ( 𝜑𝑅 ∈ Ring )
25 eqid ( 0g𝑅 ) = ( 0g𝑅 )
26 1 25 frlm0 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑋 ) → ( 𝐼 × { ( 0g𝑅 ) } ) = ( 0g𝐹 ) )
27 24 7 26 syl2anc ( 𝜑 → ( 𝐼 × { ( 0g𝑅 ) } ) = ( 0g𝐹 ) )
28 8 fveq2d ( 𝜑 → ( 0g𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
29 28 sneqd ( 𝜑 → { ( 0g𝑅 ) } = { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } )
30 29 xpeq2d ( 𝜑 → ( 𝐼 × { ( 0g𝑅 ) } ) = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) )
31 27 30 eqtr3d ( 𝜑 → ( 0g𝐹 ) = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) )
32 31 adantr ( ( 𝜑𝑦𝐵 ) → ( 0g𝐹 ) = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) )
33 32 eqeq2d ( ( 𝜑𝑦𝐵 ) → ( 𝑦 = ( 0g𝐹 ) ↔ 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) )
34 21 33 imbi12d ( ( 𝜑𝑦𝐵 ) → ( ( ( 𝐸𝑦 ) = ( 0g𝑇 ) → 𝑦 = ( 0g𝐹 ) ) ↔ ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) )
35 34 ralbidva ( 𝜑 → ( ∀ 𝑦𝐵 ( ( 𝐸𝑦 ) = ( 0g𝑇 ) → 𝑦 = ( 0g𝐹 ) ) ↔ ∀ 𝑦𝐵 ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) )
36 8 eqcomd ( 𝜑 → ( Scalar ‘ 𝑇 ) = 𝑅 )
37 36 oveq1d ( 𝜑 → ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 ) )
38 37 1 eqtr4di ( 𝜑 → ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) = 𝐹 )
39 38 fveq2d ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) = ( Base ‘ 𝐹 ) )
40 39 2 eqtr4di ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) = 𝐵 )
41 40 raleqdv ( 𝜑 → ( ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ↔ ∀ 𝑦𝐵 ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) )
42 35 41 bitr4d ( 𝜑 → ( ∀ 𝑦𝐵 ( ( 𝐸𝑦 ) = ( 0g𝑇 ) → 𝑦 = ( 0g𝐹 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ ( ( Scalar ‘ 𝑇 ) freeLMod 𝐼 ) ) ( ( 𝑇 Σg ( 𝑦f · 𝐴 ) ) = ( 0g𝑇 ) → 𝑦 = ( 𝐼 × { ( 0g ‘ ( Scalar ‘ 𝑇 ) ) } ) ) ) )
43 15 42 bitr4d ( 𝜑 → ( 𝐴 LIndF 𝑇 ↔ ∀ 𝑦𝐵 ( ( 𝐸𝑦 ) = ( 0g𝑇 ) → 𝑦 = ( 0g𝐹 ) ) ) )
44 1 2 3 4 5 6 7 8 9 frlmup1 ( 𝜑𝐸 ∈ ( 𝐹 LMHom 𝑇 ) )
45 lmghm ( 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) → 𝐸 ∈ ( 𝐹 GrpHom 𝑇 ) )
46 eqid ( 0g𝐹 ) = ( 0g𝐹 )
47 2 3 46 11 ghmf1 ( 𝐸 ∈ ( 𝐹 GrpHom 𝑇 ) → ( 𝐸 : 𝐵1-1𝐶 ↔ ∀ 𝑦𝐵 ( ( 𝐸𝑦 ) = ( 0g𝑇 ) → 𝑦 = ( 0g𝐹 ) ) ) )
48 44 45 47 3syl ( 𝜑 → ( 𝐸 : 𝐵1-1𝐶 ↔ ∀ 𝑦𝐵 ( ( 𝐸𝑦 ) = ( 0g𝑇 ) → 𝑦 = ( 0g𝐹 ) ) ) )
49 43 48 bitr4d ( 𝜑 → ( 𝐴 LIndF 𝑇𝐸 : 𝐵1-1𝐶 ) )