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 \in LMod \land I \in X \land A : I ⟶ C) \to \exists! m \in (F LMHom T) m \circ 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	$⊢ \cdot_{T} = \cdot_{T}$
7		eqid	$⊢ (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) = (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A))$
8		simp1	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to T \in LMod$
9		simp2	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to I \in X$
10	1	a1i	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to R = Scalar (T)$
11		simp3	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to A : I ⟶ C$
12	2 5 4 6 7 8 9 10 11	frlmup1	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \in (F LMHom T)$
13		ovex	$⊢ \sum_{T} (x {\cdot_{T}}_{f} A) \in V$
14	13 7	fnmpti	$⊢ (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) Fn {Base}_{F}$
15	1	lmodring	$⊢ T \in LMod \to R \in Ring$
16	15	3ad2ant1	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to R \in Ring$
17	3 2 5	uvcff	$⊢ (R \in Ring \land I \in X) \to U : I ⟶ {Base}_{F}$
18	16 9 17	syl2anc	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to U : I ⟶ {Base}_{F}$
19	18	ffnd	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to U Fn I$
20	18	frnd	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to ran U \subseteq {Base}_{F}$
21		fnco	$⊢ ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) Fn {Base}_{F} \land U Fn I \land ran U \subseteq {Base}_{F}) \to ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U) Fn I$
22	14 19 20 21	mp3an2i	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U) Fn I$
23		ffn	$⊢ A : I ⟶ C \to A Fn I$
24	23	3ad2ant3	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to A Fn I$
25	18	adantr	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to U : I ⟶ {Base}_{F}$
26	25	ffnd	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to U Fn I$
27		simpr	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to y \in I$
28		fvco2	$⊢ (U Fn I \land y \in I) \to ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U) (y) = (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) (U (y))$
29	26 27 28	syl2anc	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U) (y) = (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) (U (y))$
30		simpl1	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to T \in LMod$
31		simpl2	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to I \in X$
32	1	a1i	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to R = Scalar (T)$
33		simpl3	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to A : I ⟶ C$
34	2 5 4 6 7 30 31 32 33 27 3	frlmup2	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) (U (y)) = A (y)$
35	29 34	eqtrd	$⊢ ((T \in LMod \land I \in X \land A : I ⟶ C) \land y \in I) \to ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U) (y) = A (y)$
36	22 24 35	eqfnfvd	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U = A$
37		coeq1	$⊢ m = (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \to m \circ U = (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U$
38	37	eqeq1d	$⊢ m = (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \to (m \circ U = A \leftrightarrow (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U = A)$
39	38	rspcev	$⊢ ((x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \in (F LMHom T) \land (x \in {Base}_{F} ⟼ \sum_{T} (x {\cdot_{T}}_{f} A)) \circ U = A) \to \exists m \in (F LMHom T) m \circ U = A$
40	12 36 39	syl2anc	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to \exists m \in (F LMHom T) m \circ U = A$
41	18	ffund	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to Fun U$
42		funcoeqres	$⊢ (Fun U \land m \circ U = A) \to {m ↾}_{ran U} = A \circ U^{-1}$
43	42	ex	$⊢ Fun U \to (m \circ U = A \to {m ↾}_{ran U} = A \circ U^{-1})$
44	43	ralrimivw	$⊢ Fun U \to \forall m \in (F LMHom T) (m \circ U = A \to {m ↾}_{ran U} = A \circ U^{-1})$
45	41 44	syl	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to \forall m \in (F LMHom T) (m \circ U = A \to {m ↾}_{ran U} = A \circ U^{-1})$
46		eqid	$⊢ LBasis (F) = LBasis (F)$
47	2 3 46	frlmlbs	$⊢ (R \in Ring \land I \in X) \to ran U \in LBasis (F)$
48	16 9 47	syl2anc	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to ran U \in LBasis (F)$
49		eqid	$⊢ LSpan (F) = LSpan (F)$
50	5 46 49	lbssp	$⊢ ran U \in LBasis (F) \to LSpan (F) (ran U) = {Base}_{F}$
51	48 50	syl	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to LSpan (F) (ran U) = {Base}_{F}$
52	5 49	lspextmo	$⊢ (ran U \subseteq {Base}_{F} \land LSpan (F) (ran U) = {Base}_{F}) \to \exists^{*} m \in (F LMHom T) {m ↾}_{ran U} = A \circ U^{-1}$
53	20 51 52	syl2anc	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to \exists^{*} m \in (F LMHom T) {m ↾}_{ran U} = A \circ U^{-1}$
54		rmoim	$⊢ \forall m \in (F LMHom T) (m \circ U = A \to {m ↾}_{ran U} = A \circ U^{-1}) \to (\exists^{} m \in (F LMHom T) {m ↾}_{ran U} = A \circ U^{-1} \to \exists^{} m \in (F LMHom T) m \circ U = A)$
55	45 53 54	sylc	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to \exists^{*} m \in (F LMHom T) m \circ U = A$
56		reu5	$⊢ \exists! m \in (F LMHom T) m \circ U = A \leftrightarrow (\exists m \in (F LMHom T) m \circ U = A \land \exists^{*} m \in (F LMHom T) m \circ U = A)$
57	40 55 56	sylanbrc	$⊢ (T \in LMod \land I \in X \land A : I ⟶ C) \to \exists! m \in (F LMHom T) m \circ U = A$

Metamath Proof Explorer

Theorem frlmup4

Proof