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