Theorem frlmup4

Description: Universal property of the free module by existential uniqueness. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Hypotheses	frlmup4.r	⊢ 𝑅 = ( Scalar ‘ 𝑇 )
	frlmup4.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmup4.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
	frlmup4.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
Assertion	frlmup4	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ∃! 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		frlmup4.r	⊢ 𝑅 = ( Scalar ‘ 𝑇 )
2		frlmup4.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
3		frlmup4.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
4		frlmup4.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
5		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6		eqid	⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
7		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) )
8		simp1	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝑇 ∈ LMod )
9		simp2	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝐼 ∈ 𝑋 )
10	1	a1i	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝑅 = ( Scalar ‘ 𝑇 ) )
11		simp3	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝐴 : 𝐼 ⟶ 𝐶 )
12	2 5 4 6 7 8 9 10 11	frlmup1	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∈ ( 𝐹 LMHom 𝑇 ) )
13		ovex	⊢ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ∈ V
14	13 7	fnmpti	⊢ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) Fn ( Base ‘ 𝐹 )
15	1	lmodring	⊢ ( 𝑇 ∈ LMod → 𝑅 ∈ Ring )
16	15	3ad2ant1	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝑅 ∈ Ring )
17	3 2 5	uvcff	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) )
18	16 9 17	syl2anc	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) )
19	18	ffnd	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝑈 Fn 𝐼 )
20	18	frnd	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ran 𝑈 ⊆ ( Base ‘ 𝐹 ) )
21		fnco	⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) Fn ( Base ‘ 𝐹 ) ∧ 𝑈 Fn 𝐼 ∧ ran 𝑈 ⊆ ( Base ‘ 𝐹 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) Fn 𝐼 )
22	14 19 20 21	mp3an2i	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) Fn 𝐼 )
23		ffn	⊢ ( 𝐴 : 𝐼 ⟶ 𝐶 → 𝐴 Fn 𝐼 )
24	23	3ad2ant3	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → 𝐴 Fn 𝐼 )
25	18	adantr	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) )
26	25	ffnd	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑈 Fn 𝐼 )
27		simpr	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
28		fvco2	⊢ ( ( 𝑈 Fn 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) )
29	26 27 28	syl2anc	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) )
30		simpl1	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑇 ∈ LMod )
31		simpl2	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ 𝑋 )
32	1	a1i	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 = ( Scalar ‘ 𝑇 ) )
33		simpl3	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐶 )
34	2 5 4 6 7 30 31 32 33 27 3	frlmup2	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ‘ ( 𝑈 ‘ 𝑦 ) ) = ( 𝐴 ‘ 𝑦 ) )
35	29 34	eqtrd	⊢ ( ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
36	22 24 35	eqfnfvd	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) = 𝐴 )
37		coeq1	⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) → ( 𝑚 ∘ 𝑈 ) = ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) )
38	37	eqeq1d	⊢ ( 𝑚 = ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) → ( ( 𝑚 ∘ 𝑈 ) = 𝐴 ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) = 𝐴 ) )
39	38	rspcev	⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∈ ( 𝐹 LMHom 𝑇 ) ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↦ ( 𝑇 Σg ( 𝑥 ∘f ( ·𝑠 ‘ 𝑇 ) 𝐴 ) ) ) ∘ 𝑈 ) = 𝐴 ) → ∃ 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )
40	12 36 39	syl2anc	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ∃ 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )
41	18	ffund	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → Fun 𝑈 )
42		funcoeqres	⊢ ( ( Fun 𝑈 ∧ ( 𝑚 ∘ 𝑈 ) = 𝐴 ) → ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) )
43	42	ex	⊢ ( Fun 𝑈 → ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) ) )
44	43	ralrimivw	⊢ ( Fun 𝑈 → ∀ 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) ) )
45	41 44	syl	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ∀ 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) ) )
46		eqid	⊢ ( LBasis ‘ 𝐹 ) = ( LBasis ‘ 𝐹 )
47	2 3 46	frlmlbs	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → ran 𝑈 ∈ ( LBasis ‘ 𝐹 ) )
48	16 9 47	syl2anc	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ran 𝑈 ∈ ( LBasis ‘ 𝐹 ) )
49		eqid	⊢ ( LSpan ‘ 𝐹 ) = ( LSpan ‘ 𝐹 )
50	5 46 49	lbssp	⊢ ( ran 𝑈 ∈ ( LBasis ‘ 𝐹 ) → ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) )
51	48 50	syl	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) )
52	5 49	lspextmo	⊢ ( ( ran 𝑈 ⊆ ( Base ‘ 𝐹 ) ∧ ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) ) → ∃* 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) )
53	20 51 52	syl2anc	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ∃* 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) )
54		rmoim	⊢ ( ∀ 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( ( 𝑚 ∘ 𝑈 ) = 𝐴 → ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) ) → ( ∃* 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ↾ ran 𝑈 ) = ( 𝐴 ∘ ◡ 𝑈 ) → ∃* 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 ) )
55	45 53 54	sylc	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ∃* 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )
56		reu5	⊢ ( ∃! 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 ↔ ( ∃ 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 ∧ ∃* 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 ) )
57	40 55 56	sylanbrc	⊢ ( ( 𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴 : 𝐼 ⟶ 𝐶 ) → ∃! 𝑚 ∈ ( 𝐹 LMHom 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )