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 ๐‘‡ ) ( ๐‘š โˆ˜ ๐‘ˆ ) = ๐ด )