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 = ( Scalar ` T )
frlmup4.f 
|- F = ( R freeLMod I )
frlmup4.u 
|- U = ( R unitVec I )
frlmup4.c 
|- C = ( Base ` T )
Assertion frlmup4 
|- ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> E! m e. ( F LMHom T ) ( m o. U ) = A )

Proof

Step Hyp Ref Expression
1 frlmup4.r 
 |-  R = ( Scalar ` T )
2 frlmup4.f 
 |-  F = ( R freeLMod I )
3 frlmup4.u 
 |-  U = ( R unitVec I )
4 frlmup4.c 
 |-  C = ( Base ` T )
5 eqid 
 |-  ( Base ` F ) = ( Base ` F )
6 eqid 
 |-  ( .s ` T ) = ( .s ` T )
7 eqid 
 |-  ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) = ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) )
8 simp1 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> T e. LMod )
9 simp2 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> I e. X )
10 1 a1i 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> R = ( Scalar ` T ) )
11 simp3 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> A : I --> C )
12 2 5 4 6 7 8 9 10 11 frlmup1 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) e. ( F LMHom T ) )
13 ovex 
 |-  ( T gsum ( x oF ( .s ` T ) A ) ) e. _V
14 13 7 fnmpti 
 |-  ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) Fn ( Base ` F )
15 1 lmodring 
 |-  ( T e. LMod -> R e. Ring )
16 15 3ad2ant1 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> R e. Ring )
17 3 2 5 uvcff 
 |-  ( ( R e. Ring /\ I e. X ) -> U : I --> ( Base ` F ) )
18 16 9 17 syl2anc 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> U : I --> ( Base ` F ) )
19 18 ffnd 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> U Fn I )
20 18 frnd 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ran U C_ ( Base ` F ) )
21 fnco 
 |-  ( ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) Fn ( Base ` F ) /\ U Fn I /\ ran U C_ ( Base ` F ) ) -> ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) Fn I )
22 14 19 20 21 mp3an2i 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) Fn I )
23 ffn 
 |-  ( A : I --> C -> A Fn I )
24 23 3ad2ant3 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> A Fn I )
25 18 adantr 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> U : I --> ( Base ` F ) )
26 25 ffnd 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> U Fn I )
27 simpr 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> y e. I )
28 fvco2 
 |-  ( ( U Fn I /\ y e. I ) -> ( ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) ` y ) = ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) ` ( U ` y ) ) )
29 26 27 28 syl2anc 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> ( ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) ` y ) = ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) ` ( U ` y ) ) )
30 simpl1 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> T e. LMod )
31 simpl2 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> I e. X )
32 1 a1i 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> R = ( Scalar ` T ) )
33 simpl3 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> A : I --> C )
34 2 5 4 6 7 30 31 32 33 27 3 frlmup2 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) ` ( U ` y ) ) = ( A ` y ) )
35 29 34 eqtrd 
 |-  ( ( ( T e. LMod /\ I e. X /\ A : I --> C ) /\ y e. I ) -> ( ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) ` y ) = ( A ` y ) )
36 22 24 35 eqfnfvd 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) = A )
37 coeq1 
 |-  ( m = ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) -> ( m o. U ) = ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) )
38 37 eqeq1d 
 |-  ( m = ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) -> ( ( m o. U ) = A <-> ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) = A ) )
39 38 rspcev 
 |-  ( ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) e. ( F LMHom T ) /\ ( ( x e. ( Base ` F ) |-> ( T gsum ( x oF ( .s ` T ) A ) ) ) o. U ) = A ) -> E. m e. ( F LMHom T ) ( m o. U ) = A )
40 12 36 39 syl2anc 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> E. m e. ( F LMHom T ) ( m o. U ) = A )
41 18 ffund 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> Fun U )
42 funcoeqres 
 |-  ( ( Fun U /\ ( m o. U ) = A ) -> ( m |` ran U ) = ( A o. `' U ) )
43 42 ex 
 |-  ( Fun U -> ( ( m o. U ) = A -> ( m |` ran U ) = ( A o. `' U ) ) )
44 43 ralrimivw 
 |-  ( Fun U -> A. m e. ( F LMHom T ) ( ( m o. U ) = A -> ( m |` ran U ) = ( A o. `' U ) ) )
45 41 44 syl 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> A. m e. ( F LMHom T ) ( ( m o. U ) = A -> ( m |` ran U ) = ( A o. `' U ) ) )
46 eqid 
 |-  ( LBasis ` F ) = ( LBasis ` F )
47 2 3 46 frlmlbs 
 |-  ( ( R e. Ring /\ I e. X ) -> ran U e. ( LBasis ` F ) )
48 16 9 47 syl2anc 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ran U e. ( LBasis ` F ) )
49 eqid 
 |-  ( LSpan ` F ) = ( LSpan ` F )
50 5 46 49 lbssp 
 |-  ( ran U e. ( LBasis ` F ) -> ( ( LSpan ` F ) ` ran U ) = ( Base ` F ) )
51 48 50 syl 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> ( ( LSpan ` F ) ` ran U ) = ( Base ` F ) )
52 5 49 lspextmo 
 |-  ( ( ran U C_ ( Base ` F ) /\ ( ( LSpan ` F ) ` ran U ) = ( Base ` F ) ) -> E* m e. ( F LMHom T ) ( m |` ran U ) = ( A o. `' U ) )
53 20 51 52 syl2anc 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> E* m e. ( F LMHom T ) ( m |` ran U ) = ( A o. `' U ) )
54 rmoim 
 |-  ( A. m e. ( F LMHom T ) ( ( m o. U ) = A -> ( m |` ran U ) = ( A o. `' U ) ) -> ( E* m e. ( F LMHom T ) ( m |` ran U ) = ( A o. `' U ) -> E* m e. ( F LMHom T ) ( m o. U ) = A ) )
55 45 53 54 sylc 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> E* m e. ( F LMHom T ) ( m o. U ) = A )
56 reu5 
 |-  ( E! m e. ( F LMHom T ) ( m o. U ) = A <-> ( E. m e. ( F LMHom T ) ( m o. U ) = A /\ E* m e. ( F LMHom T ) ( m o. U ) = A ) )
57 40 55 56 sylanbrc 
 |-  ( ( T e. LMod /\ I e. X /\ A : I --> C ) -> E! m e. ( F LMHom T ) ( m o. U ) = A )