Step | Hyp | Ref
| Expression |
1 | | frlmup4.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
2 | | eqid 2824 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
3 | | frlmup4.c |
. . . 4
⊢ 𝐶 = (Base‘𝑇) |
4 | | eqid 2824 |
. . . 4
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
5 | | eqid 2824 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) |
6 | | simp1 1172 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑇 ∈ LMod) |
7 | | simp2 1173 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐼 ∈ 𝑋) |
8 | | frlmup4.r |
. . . . 5
⊢ 𝑅 = (Scalar‘𝑇) |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑅 = (Scalar‘𝑇)) |
10 | | simp3 1174 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐴:𝐼⟶𝐶) |
11 | 1, 2, 3, 4, 5, 6, 7, 9, 10 | frlmup1 20503 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∈ (𝐹 LMHom 𝑇)) |
12 | | ovex 6936 |
. . . . . . 7
⊢ (𝑇 Σg
(𝑥
∘𝑓 ( ·𝑠 ‘𝑇)𝐴)) ∈ V |
13 | 12, 5 | fnmpti 6254 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹) |
14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹)) |
15 | 8 | lmodring 19226 |
. . . . . . . 8
⊢ (𝑇 ∈ LMod → 𝑅 ∈ Ring) |
16 | 15 | 3ad2ant1 1169 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑅 ∈ Ring) |
17 | | frlmup4.u |
. . . . . . . 8
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
18 | 17, 1, 2 | uvcff 20496 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝑈:𝐼⟶(Base‘𝐹)) |
19 | 16, 7, 18 | syl2anc 581 |
. . . . . 6
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑈:𝐼⟶(Base‘𝐹)) |
20 | 19 | ffnd 6278 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑈 Fn 𝐼) |
21 | 19 | frnd 6284 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ran 𝑈 ⊆ (Base‘𝐹)) |
22 | | fnco 6231 |
. . . . 5
⊢ (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹) ∧ 𝑈 Fn 𝐼 ∧ ran 𝑈 ⊆ (Base‘𝐹)) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) Fn 𝐼) |
23 | 14, 20, 21, 22 | syl3anc 1496 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) Fn 𝐼) |
24 | | ffn 6277 |
. . . . 5
⊢ (𝐴:𝐼⟶𝐶 → 𝐴 Fn 𝐼) |
25 | 24 | 3ad2ant3 1171 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐴 Fn 𝐼) |
26 | 19 | adantr 474 |
. . . . . . 7
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑈:𝐼⟶(Base‘𝐹)) |
27 | 26 | ffnd 6278 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑈 Fn 𝐼) |
28 | | simpr 479 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
29 | | fvco2 6519 |
. . . . . 6
⊢ ((𝑈 Fn 𝐼 ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦))) |
30 | 27, 28, 29 | syl2anc 581 |
. . . . 5
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦))) |
31 | | simpl1 1248 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑇 ∈ LMod) |
32 | | simpl2 1250 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
33 | 8 | a1i 11 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑅 = (Scalar‘𝑇)) |
34 | | simpl3 1252 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝐴:𝐼⟶𝐶) |
35 | 1, 2, 3, 4, 5, 31,
32, 33, 34, 28, 17 | frlmup2 20504 |
. . . . 5
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦)) = (𝐴‘𝑦)) |
36 | 30, 35 | eqtrd 2860 |
. . . 4
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = (𝐴‘𝑦)) |
37 | 23, 25, 36 | eqfnfvd 6562 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴) |
38 | | coeq1 5511 |
. . . . 5
⊢ (𝑚 = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) → (𝑚 ∘ 𝑈) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)) |
39 | 38 | eqeq1d 2826 |
. . . 4
⊢ (𝑚 = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) → ((𝑚 ∘ 𝑈) = 𝐴 ↔ ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴)) |
40 | 39 | rspcev 3525 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∈ (𝐹 LMHom 𝑇) ∧ ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴) → ∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
41 | 11, 37, 40 | syl2anc 581 |
. 2
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
42 | 19 | ffund 6281 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → Fun 𝑈) |
43 | | funcoeqres 6407 |
. . . . . 6
⊢ ((Fun
𝑈 ∧ (𝑚 ∘ 𝑈) = 𝐴) → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
44 | 43 | ex 403 |
. . . . 5
⊢ (Fun
𝑈 → ((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
45 | 44 | ralrimivw 3175 |
. . . 4
⊢ (Fun
𝑈 → ∀𝑚 ∈ (𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
46 | 42, 45 | syl 17 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∀𝑚 ∈ (𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
47 | | eqid 2824 |
. . . . . . 7
⊢
(LBasis‘𝐹) =
(LBasis‘𝐹) |
48 | 1, 17, 47 | frlmlbs 20502 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → ran 𝑈 ∈ (LBasis‘𝐹)) |
49 | 16, 7, 48 | syl2anc 581 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ran 𝑈 ∈ (LBasis‘𝐹)) |
50 | | eqid 2824 |
. . . . . 6
⊢
(LSpan‘𝐹) =
(LSpan‘𝐹) |
51 | 2, 47, 50 | lbssp 19437 |
. . . . 5
⊢ (ran
𝑈 ∈
(LBasis‘𝐹) →
((LSpan‘𝐹)‘ran
𝑈) = (Base‘𝐹)) |
52 | 49, 51 | syl 17 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) |
53 | 2, 50 | lspextmo 19414 |
. . . 4
⊢ ((ran
𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
54 | 21, 52, 53 | syl2anc 581 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
55 | | rmoim 3633 |
. . 3
⊢
(∀𝑚 ∈
(𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) → (∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴)) |
56 | 46, 54, 55 | sylc 65 |
. 2
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
57 | | reu5 3370 |
. 2
⊢
(∃!𝑚 ∈
(𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴 ↔ (∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴 ∧ ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴)) |
58 | 41, 56, 57 | sylanbrc 580 |
1
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃!𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |