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

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→ 𝐶 ) )