Metamath Proof Explorer

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 𝑇 ) ( 𝑚 ∘ 𝑈 ) = 𝐴 )