Step | Hyp | Ref
| Expression |
1 | | frlmup4.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
3 | | frlmup4.c |
. . . 4
⊢ 𝐶 = (Base‘𝑇) |
4 | | eqid 2610 |
. . . 4
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
5 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) |
6 | | simp1 1054 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑇 ∈ LMod) |
7 | | simp2 1055 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐼 ∈ 𝑋) |
8 | | frlmup4.r |
. . . . 5
⊢ 𝑅 = (Scalar‘𝑇) |
9 | 8 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑅 = (Scalar‘𝑇)) |
10 | | simp3 1056 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐴:𝐼⟶𝐶) |
11 | 1, 2, 3, 4, 5, 6, 7, 9, 10 | frlmup1 19956 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∈ (𝐹 LMHom 𝑇)) |
12 | | ovex 6577 |
. . . . . . 7
⊢ (𝑇 Σg
(𝑥
∘𝑓 ( ·𝑠 ‘𝑇)𝐴)) ∈ V |
13 | 12, 5 | fnmpti 5935 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹) |
14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹)) |
15 | 8 | lmodring 18694 |
. . . . . . . 8
⊢ (𝑇 ∈ LMod → 𝑅 ∈ Ring) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑅 ∈ Ring) |
17 | | frlmup4.u |
. . . . . . . 8
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
18 | 17, 1, 2 | uvcff 19949 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝑈:𝐼⟶(Base‘𝐹)) |
19 | 16, 7, 18 | syl2anc 691 |
. . . . . 6
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑈:𝐼⟶(Base‘𝐹)) |
20 | | ffn 5958 |
. . . . . 6
⊢ (𝑈:𝐼⟶(Base‘𝐹) → 𝑈 Fn 𝐼) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝑈 Fn 𝐼) |
22 | | frn 5966 |
. . . . . 6
⊢ (𝑈:𝐼⟶(Base‘𝐹) → ran 𝑈 ⊆ (Base‘𝐹)) |
23 | 19, 22 | syl 17 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ran 𝑈 ⊆ (Base‘𝐹)) |
24 | | fnco 5913 |
. . . . 5
⊢ (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) Fn (Base‘𝐹) ∧ 𝑈 Fn 𝐼 ∧ ran 𝑈 ⊆ (Base‘𝐹)) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) Fn 𝐼) |
25 | 14, 21, 23, 24 | syl3anc 1318 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) Fn 𝐼) |
26 | | ffn 5958 |
. . . . 5
⊢ (𝐴:𝐼⟶𝐶 → 𝐴 Fn 𝐼) |
27 | 26 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → 𝐴 Fn 𝐼) |
28 | 19 | adantr 480 |
. . . . . . 7
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑈:𝐼⟶(Base‘𝐹)) |
29 | 28, 20 | syl 17 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑈 Fn 𝐼) |
30 | | simpr 476 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
31 | | fvco2 6183 |
. . . . . 6
⊢ ((𝑈 Fn 𝐼 ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦))) |
32 | 29, 30, 31 | syl2anc 691 |
. . . . 5
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦))) |
33 | | simpl1 1057 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑇 ∈ LMod) |
34 | | simpl2 1058 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
35 | 8 | a1i 11 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝑅 = (Scalar‘𝑇)) |
36 | | simpl3 1059 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → 𝐴:𝐼⟶𝐶) |
37 | 1, 2, 3, 4, 5, 33,
34, 35, 36, 30, 17 | frlmup2 19957 |
. . . . 5
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴)))‘(𝑈‘𝑦)) = (𝐴‘𝑦)) |
38 | 32, 37 | eqtrd 2644 |
. . . 4
⊢ (((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) ∧ 𝑦 ∈ 𝐼) → (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)‘𝑦) = (𝐴‘𝑦)) |
39 | 25, 27, 38 | eqfnfvd 6222 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴) |
40 | | coeq1 5201 |
. . . . 5
⊢ (𝑚 = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) → (𝑚 ∘ 𝑈) = ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈)) |
41 | 40 | eqeq1d 2612 |
. . . 4
⊢ (𝑚 = (𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) → ((𝑚 ∘ 𝑈) = 𝐴 ↔ ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴)) |
42 | 41 | rspcev 3282 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∈ (𝐹 LMHom 𝑇) ∧ ((𝑥 ∈ (Base‘𝐹) ↦ (𝑇 Σg (𝑥 ∘𝑓 (
·𝑠 ‘𝑇)𝐴))) ∘ 𝑈) = 𝐴) → ∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
43 | 11, 39, 42 | syl2anc 691 |
. 2
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
44 | | ffun 5961 |
. . . . 5
⊢ (𝑈:𝐼⟶(Base‘𝐹) → Fun 𝑈) |
45 | 19, 44 | syl 17 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → Fun 𝑈) |
46 | | funcoeqres 6080 |
. . . . . 6
⊢ ((Fun
𝑈 ∧ (𝑚 ∘ 𝑈) = 𝐴) → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
47 | 46 | ex 449 |
. . . . 5
⊢ (Fun
𝑈 → ((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
48 | 47 | ralrimivw 2950 |
. . . 4
⊢ (Fun
𝑈 → ∀𝑚 ∈ (𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
49 | 45, 48 | syl 17 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∀𝑚 ∈ (𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈))) |
50 | | eqid 2610 |
. . . . . . 7
⊢
(LBasis‘𝐹) =
(LBasis‘𝐹) |
51 | 1, 17, 50 | frlmlbs 19955 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → ran 𝑈 ∈ (LBasis‘𝐹)) |
52 | 16, 7, 51 | syl2anc 691 |
. . . . 5
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ran 𝑈 ∈ (LBasis‘𝐹)) |
53 | | eqid 2610 |
. . . . . 6
⊢
(LSpan‘𝐹) =
(LSpan‘𝐹) |
54 | 2, 50, 53 | lbssp 18900 |
. . . . 5
⊢ (ran
𝑈 ∈
(LBasis‘𝐹) →
((LSpan‘𝐹)‘ran
𝑈) = (Base‘𝐹)) |
55 | 52, 54 | syl 17 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) |
56 | 2, 53 | lspextmo 18877 |
. . . 4
⊢ ((ran
𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
57 | 23, 55, 56 | syl2anc 691 |
. . 3
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) |
58 | | rmoim 3374 |
. . 3
⊢
(∀𝑚 ∈
(𝐹 LMHom 𝑇)((𝑚 ∘ 𝑈) = 𝐴 → (𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈)) → (∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ↾ ran 𝑈) = (𝐴 ∘ ◡𝑈) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴)) |
59 | 49, 57, 58 | sylc 63 |
. 2
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |
60 | | reu5 3136 |
. 2
⊢
(∃!𝑚 ∈
(𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴 ↔ (∃𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴 ∧ ∃*𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴)) |
61 | 43, 59, 60 | sylanbrc 695 |
1
⊢ ((𝑇 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐴:𝐼⟶𝐶) → ∃!𝑚 ∈ (𝐹 LMHom 𝑇)(𝑚 ∘ 𝑈) = 𝐴) |