Step | Hyp | Ref
| Expression |
1 | | frlmup4.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
2 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
3 | | frlmup4.c |
. . . 4
⊢ 𝐶 = (Base‘𝑇) |
4 | | eqid 2738 |
. . . 4
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
5 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) |
6 | | simp1 1135 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑇 ∈ LMod) |
7 | | simp2 1136 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐼 ∈ 𝑋) |
8 | | frlmup4.r |
. . . . 5
⊢ 𝑅 = (Scalar‘𝑇) |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑅 = (Scalar‘𝑇)) |
10 | | simp3 1137 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐴:𝐼⟶𝐶) |
11 | 1, 2, 3, 4, 5, 6, 7, 9, 10 | frlmup1 21005 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∈ (𝐹 LMHom 𝑇)) |
12 | | ovex 7308 |
. . . . . 6
⊢ (𝑇 Σg
(𝑥 ∘f (
·𝑠 ‘𝑇)𝐴)) ∈ V |
13 | 12, 5 | fnmpti 6576 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹) |
14 | 8 | lmodring 20131 |
. . . . . . . 8
⊢ (𝑇 ∈ LMod → 𝑅 ∈ Ring) |
15 | 14 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑅 ∈ Ring) |
16 | | frlmup4.u |
. . . . . . . 8
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
17 | 16, 1, 2 | uvcff 20998 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝑈:𝐼⟶(Base‘𝐹)) |
18 | 15, 7, 17 | syl2anc 584 |
. . . . . 6
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑈:𝐼⟶(Base‘𝐹)) |
19 | 18 | ffnd 6601 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑈 Fn 𝐼) |
20 | 18 | frnd 6608 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ran 𝑈 ⊆ (Base‘𝐹)) |
21 | | fnco 6549 |
. . . . 5
⊢ (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹) ∧ 𝑈 Fn 𝐼 ∧ ran 𝑈 ⊆ (Base‘𝐹)) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) Fn 𝐼) |
22 | 13, 19, 20, 21 | mp3an2i 1465 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) Fn 𝐼) |
23 | | ffn 6600 |
. . . . 5
⊢ (𝐴:𝐼⟶𝐶 → 𝐴 Fn 𝐼) |
24 | 23 | 3ad2ant3 1134 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐴 Fn 𝐼) |
25 | 18 | adantr 481 |
. . . . . . 7
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑈:𝐼⟶(Base‘𝐹)) |
26 | 25 | ffnd 6601 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑈 Fn 𝐼) |
27 | | simpr 485 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
28 | | fvco2 6865 |
. . . . . 6
⊢ ((𝑈 Fn 𝐼 ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦))) |
29 | 26, 27, 28 | syl2anc 584 |
. . . . 5
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦))) |
30 | | simpl1 1190 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑇 ∈ LMod) |
31 | | simpl2 1191 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
32 | 8 | a1i 11 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑅 = (Scalar‘𝑇)) |
33 | | simpl3 1192 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝐴:𝐼⟶𝐶) |
34 | 1, 2, 3, 4, 5, 30,
31, 32, 33, 27, 16 | frlmup2 21006 |
. . . . 5
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦)) = (𝐴‘𝑦)) |
35 | 29, 34 | eqtrd 2778 |
. . . 4
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = (𝐴‘𝑦)) |
36 | 22, 24, 35 | eqfnfvd 6912 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴) |
37 | | coeq1 5766 |
. . . . 5
⊢ (𝑚 = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) → (𝑚 ∘ 𝑈) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)) |
38 | 37 | eqeq1d 2740 |
. . . 4
⊢ (𝑚 = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) → ((𝑚 ∘ 𝑈) = 𝐴 ↔ ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴)) |
39 | 38 | rspcev 3561 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∈ (𝐹 LMHom 𝑇) ∧ ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘f (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴) → ∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
40 | 11, 36, 39 | syl2anc 584 |
. 2
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
41 | 18 | ffund 6604 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → Fun 𝑈) |
42 | | funcoeqres 6747 |
. . . . . 6
⊢ ((Fun
𝑈 ∧ (𝑚 ∘ 𝑈) = 𝐴) → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
43 | 42 | ex 413 |
. . . . 5
⊢ (Fun
𝑈 → ((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
44 | 43 | ralrimivw 3104 |
. . . 4
⊢ (Fun
𝑈 → ∀𝑚 ∈ (𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
45 | 41, 44 | syl 17 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∀𝑚 ∈ (𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
46 | | eqid 2738 |
. . . . . . 7
⊢
(LBasis‘𝐹) =
(LBasis‘𝐹) |
47 | 1, 16, 46 | frlmlbs 21004 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → ran 𝑈 ∈ (LBasis‘𝐹)) |
48 | 15, 7, 47 | syl2anc 584 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ran 𝑈 ∈ (LBasis‘𝐹)) |
49 | | eqid 2738 |
. . . . . 6
⊢
(LSpan‘𝐹) =
(LSpan‘𝐹) |
50 | 2, 46, 49 | lbssp 20341 |
. . . . 5
⊢ (ran
𝑈 ∈
(LBasis‘𝐹) →
((LSpan‘𝐹)‘ran
𝑈) = (Base‘𝐹)) |
51 | 48, 50 | syl 17 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) |
52 | 2, 49 | lspextmo 20318 |
. . . 4
⊢ ((ran
𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
53 | 20, 51, 52 | syl2anc 584 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
54 | | rmoim 3675 |
. . 3
⊢
(∀𝑚 ∈
(𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) → (∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴)) |
55 | 45, 53, 54 | sylc 65 |
. 2
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
56 | | reu5 3361 |
. 2
⊢
(∃!𝑚 ∈
(𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴 ↔ (∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴 ∧ ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴)) |
57 | 40, 55, 56 | sylanbrc 583 |
1
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃!𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |