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 R=ScalarT
frlmup4.f F=RfreeLModI
frlmup4.u U=RunitVecI
frlmup4.c C=BaseT
Assertion frlmup4 TLModIXA:IC∃!mFLMHomTmU=A

Proof

Step Hyp Ref Expression
1 frlmup4.r R=ScalarT
2 frlmup4.f F=RfreeLModI
3 frlmup4.u U=RunitVecI
4 frlmup4.c C=BaseT
5 eqid BaseF=BaseF
6 eqid T=T
7 eqid xBaseFTxTfA=xBaseFTxTfA
8 simp1 TLModIXA:ICTLMod
9 simp2 TLModIXA:ICIX
10 1 a1i TLModIXA:ICR=ScalarT
11 simp3 TLModIXA:ICA:IC
12 2 5 4 6 7 8 9 10 11 frlmup1 TLModIXA:ICxBaseFTxTfAFLMHomT
13 ovex TxTfAV
14 13 7 fnmpti xBaseFTxTfAFnBaseF
15 1 lmodring TLModRRing
16 15 3ad2ant1 TLModIXA:ICRRing
17 3 2 5 uvcff RRingIXU:IBaseF
18 16 9 17 syl2anc TLModIXA:ICU:IBaseF
19 18 ffnd TLModIXA:ICUFnI
20 18 frnd TLModIXA:ICranUBaseF
21 fnco xBaseFTxTfAFnBaseFUFnIranUBaseFxBaseFTxTfAUFnI
22 14 19 20 21 mp3an2i TLModIXA:ICxBaseFTxTfAUFnI
23 ffn A:ICAFnI
24 23 3ad2ant3 TLModIXA:ICAFnI
25 18 adantr TLModIXA:ICyIU:IBaseF
26 25 ffnd TLModIXA:ICyIUFnI
27 simpr TLModIXA:ICyIyI
28 fvco2 UFnIyIxBaseFTxTfAUy=xBaseFTxTfAUy
29 26 27 28 syl2anc TLModIXA:ICyIxBaseFTxTfAUy=xBaseFTxTfAUy
30 simpl1 TLModIXA:ICyITLMod
31 simpl2 TLModIXA:ICyIIX
32 1 a1i TLModIXA:ICyIR=ScalarT
33 simpl3 TLModIXA:ICyIA:IC
34 2 5 4 6 7 30 31 32 33 27 3 frlmup2 TLModIXA:ICyIxBaseFTxTfAUy=Ay
35 29 34 eqtrd TLModIXA:ICyIxBaseFTxTfAUy=Ay
36 22 24 35 eqfnfvd TLModIXA:ICxBaseFTxTfAU=A
37 coeq1 m=xBaseFTxTfAmU=xBaseFTxTfAU
38 37 eqeq1d m=xBaseFTxTfAmU=AxBaseFTxTfAU=A
39 38 rspcev xBaseFTxTfAFLMHomTxBaseFTxTfAU=AmFLMHomTmU=A
40 12 36 39 syl2anc TLModIXA:ICmFLMHomTmU=A
41 18 ffund TLModIXA:ICFunU
42 funcoeqres FunUmU=AmranU=AU-1
43 42 ex FunUmU=AmranU=AU-1
44 43 ralrimivw FunUmFLMHomTmU=AmranU=AU-1
45 41 44 syl TLModIXA:ICmFLMHomTmU=AmranU=AU-1
46 eqid LBasisF=LBasisF
47 2 3 46 frlmlbs RRingIXranULBasisF
48 16 9 47 syl2anc TLModIXA:ICranULBasisF
49 eqid LSpanF=LSpanF
50 5 46 49 lbssp ranULBasisFLSpanFranU=BaseF
51 48 50 syl TLModIXA:ICLSpanFranU=BaseF
52 5 49 lspextmo ranUBaseFLSpanFranU=BaseF*mFLMHomTmranU=AU-1
53 20 51 52 syl2anc TLModIXA:IC*mFLMHomTmranU=AU-1
54 rmoim mFLMHomTmU=AmranU=AU-1*mFLMHomTmranU=AU-1*mFLMHomTmU=A
55 45 53 54 sylc TLModIXA:IC*mFLMHomTmU=A
56 reu5 ∃!mFLMHomTmU=AmFLMHomTmU=A*mFLMHomTmU=A
57 40 55 56 sylanbrc TLModIXA:IC∃!mFLMHomTmU=A