Description: Universal property of the free module by existential uniqueness. (Contributed by Stefan O'Rear, 7-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frlmup4.r | |
|
frlmup4.f | |
||
frlmup4.u | |
||
frlmup4.c | |
||
Assertion | frlmup4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frlmup4.r | |
|
2 | frlmup4.f | |
|
3 | frlmup4.u | |
|
4 | frlmup4.c | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | simp1 | |
|
9 | simp2 | |
|
10 | 1 | a1i | |
11 | simp3 | |
|
12 | 2 5 4 6 7 8 9 10 11 | frlmup1 | |
13 | ovex | |
|
14 | 13 7 | fnmpti | |
15 | 1 | lmodring | |
16 | 15 | 3ad2ant1 | |
17 | 3 2 5 | uvcff | |
18 | 16 9 17 | syl2anc | |
19 | 18 | ffnd | |
20 | 18 | frnd | |
21 | fnco | |
|
22 | 14 19 20 21 | mp3an2i | |
23 | ffn | |
|
24 | 23 | 3ad2ant3 | |
25 | 18 | adantr | |
26 | 25 | ffnd | |
27 | simpr | |
|
28 | fvco2 | |
|
29 | 26 27 28 | syl2anc | |
30 | simpl1 | |
|
31 | simpl2 | |
|
32 | 1 | a1i | |
33 | simpl3 | |
|
34 | 2 5 4 6 7 30 31 32 33 27 3 | frlmup2 | |
35 | 29 34 | eqtrd | |
36 | 22 24 35 | eqfnfvd | |
37 | coeq1 | |
|
38 | 37 | eqeq1d | |
39 | 38 | rspcev | |
40 | 12 36 39 | syl2anc | |
41 | 18 | ffund | |
42 | funcoeqres | |
|
43 | 42 | ex | |
44 | 43 | ralrimivw | |
45 | 41 44 | syl | |
46 | eqid | |
|
47 | 2 3 46 | frlmlbs | |
48 | 16 9 47 | syl2anc | |
49 | eqid | |
|
50 | 5 46 49 | lbssp | |
51 | 48 50 | syl | |
52 | 5 49 | lspextmo | |
53 | 20 51 52 | syl2anc | |
54 | rmoim | |
|
55 | 45 53 54 | sylc | |
56 | reu5 | |
|
57 | 40 55 56 | sylanbrc | |