Step | Hyp | Ref
| Expression |
1 | | frlmphl.v |
. . 3
⊢ 𝑉 = (Base‘𝑌) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝑉 = (Base‘𝑌)) |
3 | | eqidd 2611 |
. 2
⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌)) |
4 | | eqidd 2611 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌)) |
5 | | frlmphl.j |
. . 3
⊢ , =
(·𝑖‘𝑌) |
6 | 5 | a1i 11 |
. 2
⊢ (𝜑 → , =
(·𝑖‘𝑌)) |
7 | | frlmphl.o |
. . 3
⊢ 𝑂 = (0g‘𝑌) |
8 | 7 | a1i 11 |
. 2
⊢ (𝜑 → 𝑂 = (0g‘𝑌)) |
9 | | frlmphl.f |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Field) |
10 | | isfld 18579 |
. . . . 5
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
11 | 9, 10 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
12 | 11 | simpld 474 |
. . 3
⊢ (𝜑 → 𝑅 ∈ DivRing) |
13 | | frlmphl.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
14 | | frlmphl.y |
. . . 4
⊢ 𝑌 = (𝑅 freeLMod 𝐼) |
15 | 14 | frlmsca 19916 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊) → 𝑅 = (Scalar‘𝑌)) |
16 | 12, 13, 15 | syl2anc 691 |
. 2
⊢ (𝜑 → 𝑅 = (Scalar‘𝑌)) |
17 | | frlmphl.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
18 | 17 | a1i 11 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
19 | | eqidd 2611 |
. 2
⊢ (𝜑 → (+g‘𝑅) = (+g‘𝑅)) |
20 | | frlmphl.t |
. . 3
⊢ · =
(.r‘𝑅) |
21 | 20 | a1i 11 |
. 2
⊢ (𝜑 → · =
(.r‘𝑅)) |
22 | | frlmphl.s |
. . 3
⊢ ∗ =
(*𝑟‘𝑅) |
23 | 22 | a1i 11 |
. 2
⊢ (𝜑 → ∗ =
(*𝑟‘𝑅)) |
24 | | frlmphl.0 |
. . 3
⊢ 0 =
(0g‘𝑅) |
25 | 24 | a1i 11 |
. 2
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
26 | | drngring 18577 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
27 | 12, 26 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
28 | 14 | frlmlmod 19912 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ LMod) |
29 | 27, 13, 28 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑌 ∈ LMod) |
30 | 16, 12 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (Scalar‘𝑌) ∈
DivRing) |
31 | | eqid 2610 |
. . . 4
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
32 | 31 | islvec 18925 |
. . 3
⊢ (𝑌 ∈ LVec ↔ (𝑌 ∈ LMod ∧
(Scalar‘𝑌) ∈
DivRing)) |
33 | 29, 30, 32 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝑌 ∈ LVec) |
34 | 11 | simprd 478 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
35 | | frlmphl.u |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥) |
36 | 17, 22, 34, 35 | idsrngd 18685 |
. 2
⊢ (𝜑 → 𝑅 ∈ *-Ring) |
37 | 13 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝐼 ∈ 𝑊) |
38 | 27 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ Ring) |
39 | | simp2 1055 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ 𝑉) |
40 | | simp3 1056 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ 𝑉) |
41 | 14, 17, 20, 1, 5 | frlmipval 19937 |
. . . . 5
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉)) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘𝑓
·
ℎ))) |
42 | 37, 38, 39, 40, 41 | syl22anc 1319 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘𝑓
·
ℎ))) |
43 | 14, 17, 1 | frlmbasmap 19922 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) |
44 | 37, 39, 43 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) |
45 | | elmapi 7765 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) → 𝑔:𝐼⟶𝐵) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔:𝐼⟶𝐵) |
47 | | ffn 5958 |
. . . . . . 7
⊢ (𝑔:𝐼⟶𝐵 → 𝑔 Fn 𝐼) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 Fn 𝐼) |
49 | 14, 17, 1 | frlmbasmap 19922 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑𝑚 𝐼)) |
50 | 37, 40, 49 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑𝑚 𝐼)) |
51 | | elmapi 7765 |
. . . . . . . 8
⊢ (ℎ ∈ (𝐵 ↑𝑚 𝐼) → ℎ:𝐼⟶𝐵) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ:𝐼⟶𝐵) |
53 | | ffn 5958 |
. . . . . . 7
⊢ (ℎ:𝐼⟶𝐵 → ℎ Fn 𝐼) |
54 | 52, 53 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ Fn 𝐼) |
55 | | inidm 3784 |
. . . . . 6
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
56 | | eqidd 2611 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
57 | | eqidd 2611 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
58 | 48, 54, 37, 37, 55, 56, 57 | offval 6802 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 ∘𝑓 · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
59 | 58 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑔 ∘𝑓
·
ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
60 | 42, 59 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
61 | | ringcmn 18404 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
62 | 27, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
63 | 62 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CMnd) |
64 | 38 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
65 | 46 | ffvelrnda 6267 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵) |
66 | 52 | ffvelrnda 6267 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵) |
67 | 17, 20 | ringcl 18384 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵) |
68 | 64, 65, 66, 67 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵) |
69 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) |
70 | 68, 69 | fmptd 6292 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))):𝐼⟶𝐵) |
71 | | frlmphl.m |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) |
72 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 19938 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 ) |
73 | 17, 24, 63, 37, 70, 72 | gsumcl 18139 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) ∈ 𝐵) |
74 | 60, 73 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) ∈ 𝐵) |
75 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
76 | 62 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ CMnd) |
77 | 13 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐼 ∈ 𝑊) |
78 | 27 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ Ring) |
79 | 78 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
80 | | simp2 1055 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ 𝐵) |
81 | 80 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑘 ∈ 𝐵) |
82 | | simp31 1090 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ 𝑉) |
83 | 77, 82, 43 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) |
84 | 83, 45 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔:𝐼⟶𝐵) |
85 | 84 | ffvelrnda 6267 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵) |
86 | | simp33 1092 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ 𝑉) |
87 | 14, 17, 1 | frlmbasmap 19922 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ (𝐵 ↑𝑚 𝐼)) |
88 | 77, 86, 87 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ (𝐵 ↑𝑚 𝐼)) |
89 | | elmapi 7765 |
. . . . . . . 8
⊢ (𝑖 ∈ (𝐵 ↑𝑚 𝐼) → 𝑖:𝐼⟶𝐵) |
90 | 88, 89 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖:𝐼⟶𝐵) |
91 | 90 | ffvelrnda 6267 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) ∈ 𝐵) |
92 | 17, 20 | ringcl 18384 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
93 | 79, 85, 91, 92 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
94 | 17, 20 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵) |
95 | 79, 81, 93, 94 | syl3anc 1318 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵) |
96 | | simp32 1091 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ 𝑉) |
97 | 77, 96, 49 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ (𝐵 ↑𝑚 𝐼)) |
98 | 97, 51 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ:𝐼⟶𝐵) |
99 | 98 | ffvelrnda 6267 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵) |
100 | 17, 20 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
101 | 79, 99, 91, 100 | syl3anc 1318 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
102 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
103 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) |
104 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦)) |
105 | 104 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑘 · (𝑔‘𝑥)) = (𝑘 · (𝑔‘𝑦))) |
106 | 105 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) |
107 | 106 | oveq1i 6559 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) = ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘𝑓 · 𝑖) |
108 | 17, 20 | ringcl 18384 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵) |
109 | 79, 81, 85, 108 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵) |
110 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) |
111 | 109, 110 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))):𝐼⟶𝐵) |
112 | | ffn 5958 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))):𝐼⟶𝐵 → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼) |
113 | 111, 112 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼) |
114 | 106 | fneq1i 5899 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼 ↔ (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼) |
115 | 113, 114 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼) |
116 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑖:𝐼⟶𝐵 → 𝑖 Fn 𝐼) |
117 | 90, 116 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 Fn 𝐼) |
118 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))) |
119 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
120 | 119 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑔‘𝑦) = (𝑔‘𝑥)) |
121 | 120 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑘 · (𝑔‘𝑦)) = (𝑘 · (𝑔‘𝑥))) |
122 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
123 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑘 · (𝑔‘𝑥)) ∈ V |
124 | 123 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ V) |
125 | 118, 121,
122, 124 | fvmptd 6197 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))‘𝑥) = (𝑘 · (𝑔‘𝑥))) |
126 | | eqidd 2611 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) = (𝑖‘𝑥)) |
127 | 115, 117,
77, 77, 55, 125, 126 | offval 6802 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘𝑓 · 𝑖) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)))) |
128 | 17, 20 | ringass 18387 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
129 | 79, 81, 85, 91, 128 | syl13anc 1320 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
130 | 129 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
131 | 127, 130 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘𝑓 · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
132 | 107, 131 | syl5eq 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
133 | | ovex 6577 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ∈ V |
134 | 133 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ∈ V) |
135 | | funmpt 5840 |
. . . . . . 7
⊢ Fun
(𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧))) |
136 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑧 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) = ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧)) |
137 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑧 ∈ 𝐼) → (𝑖‘𝑧) = (𝑖‘𝑧)) |
138 | 113, 117,
77, 77, 55, 136, 137 | offval 6802 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) = (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧)))) |
139 | 138 | funeqd 5825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ↔ Fun (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧))))) |
140 | 135, 139 | mpbiri 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖)) |
141 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ 𝑉) |
142 | 13, 141 | anim12i 588 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉)) |
143 | 142 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉)) |
144 | 14, 24, 1 | frlmbasfsupp 19921 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 finSupp 0 ) |
145 | 143, 144 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 finSupp 0 ) |
146 | 17, 24 | ring0cl 18392 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
147 | 78, 146 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 0 ∈ 𝐵) |
148 | 17, 20, 24 | ringrz 18411 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 ) |
149 | 78, 148 | sylan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 ) |
150 | 77, 147, 111, 90, 149 | suppofss2d 7220 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 )) |
151 | | fsuppsssupp 8174 |
. . . . . 6
⊢
(((((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ∈ V ∧ Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖)) ∧ (𝑖 finSupp 0 ∧ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) finSupp 0 ) |
152 | 134, 140,
145, 150, 151 | syl22anc 1319 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) finSupp 0 ) |
153 | 132, 152 | eqbrtrrd 4607 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) finSupp 0 ) |
154 | | simp1 1054 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝜑) |
155 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑔 = ℎ → (𝑔 ∈ 𝑉 ↔ ℎ ∈ 𝑉)) |
156 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑔 = ℎ → 𝑔 = ℎ) |
157 | 156, 156 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑔 = ℎ → (𝑔 , 𝑔) = (ℎ , ℎ)) |
158 | 157 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑔 = ℎ → ((𝑔 , 𝑔) = 0 ↔ (ℎ , ℎ) = 0 )) |
159 | 155, 158 | 3anbi23d 1394 |
. . . . . . . 8
⊢ (𝑔 = ℎ → ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) ↔ (𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ))) |
160 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑔 = ℎ → (𝑔 = 𝑂 ↔ ℎ = 𝑂)) |
161 | 159, 160 | imbi12d 333 |
. . . . . . 7
⊢ (𝑔 = ℎ → (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) ↔ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂))) |
162 | 161, 71 | chvarv 2251 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂) |
163 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 162, 35, 13 | frlmphllem 19938 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
164 | 154, 96, 86, 163 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
165 | 17, 24, 75, 76, 77, 95, 101, 102, 103, 153, 164 | gsummptfsadd 18147 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
166 | 14, 17, 20 | frlmip 19936 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ DivRing) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) =
(·𝑖‘𝑌)) |
167 | 13, 12, 166 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) =
(·𝑖‘𝑌)) |
168 | 167, 5 | syl6reqr 2663 |
. . . . . . 7
⊢ (𝜑 → , = (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))) |
169 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑔 → (𝑒‘𝑥) = (𝑔‘𝑥)) |
170 | 169 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑔 → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑓‘𝑥))) |
171 | 170 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑒 = 𝑔 → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) |
172 | 171 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑒 = 𝑔 → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))))) |
173 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑓 = ℎ → (𝑓‘𝑥) = (ℎ‘𝑥)) |
174 | 173 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑓 = ℎ → ((𝑔‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
175 | 174 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑓 = ℎ → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
176 | 175 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑓 = ℎ → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
177 | 172, 176 | cbvmpt2v 6633 |
. . . . . . 7
⊢ (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
178 | 168, 177 | syl6eqr 2662 |
. . . . . 6
⊢ (𝜑 → , = (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
179 | 178 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → , = (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
180 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)) |
181 | 180 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥)) |
182 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
183 | 182 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
184 | 181, 183 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) |
185 | 184 | mpteq2dv 4673 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) |
186 | 185 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))) |
187 | 29 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑌 ∈ LMod) |
188 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 = (Scalar‘𝑌)) |
189 | 188 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Base‘𝑅) = (Base‘(Scalar‘𝑌))) |
190 | 17, 189 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐵 = (Base‘(Scalar‘𝑌))) |
191 | 80, 190 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ (Base‘(Scalar‘𝑌))) |
192 | | eqid 2610 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
193 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
194 | 1, 31, 192, 193 | lmodvscl 18703 |
. . . . . . . 8
⊢ ((𝑌 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑔 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) |
195 | 187, 191,
82, 194 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) |
196 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝑌) = (+g‘𝑌) |
197 | 1, 196 | lmodvacl 18700 |
. . . . . . 7
⊢ ((𝑌 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑌)𝑔) ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) |
198 | 187, 195,
96, 197 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) |
199 | 14, 17, 1 | frlmbasmap 19922 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑𝑚 𝐼)) |
200 | 77, 198, 199 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑𝑚 𝐼)) |
201 | | ovex 6577 |
. . . . . 6
⊢ (𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) ∈ V |
202 | 201 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
203 | 179, 186,
200, 88, 202 | ovmpt2d 6686 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))) |
204 | 14, 1, 78, 77, 195, 96, 75, 196 | frlmplusgval 19926 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) = ((𝑘( ·𝑠
‘𝑌)𝑔) ∘𝑓
(+g‘𝑅)ℎ)) |
205 | 14, 17, 1 | frlmbasmap 19922 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ (𝐵 ↑𝑚 𝐼)) |
206 | 77, 195, 205 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ (𝐵 ↑𝑚 𝐼)) |
207 | | elmapi 7765 |
. . . . . . . . . . . 12
⊢ ((𝑘(
·𝑠 ‘𝑌)𝑔) ∈ (𝐵 ↑𝑚 𝐼) → (𝑘( ·𝑠
‘𝑌)𝑔):𝐼⟶𝐵) |
208 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ ((𝑘(
·𝑠 ‘𝑌)𝑔):𝐼⟶𝐵 → (𝑘( ·𝑠
‘𝑌)𝑔) Fn 𝐼) |
209 | 206, 207,
208 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) Fn 𝐼) |
210 | 98, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ Fn 𝐼) |
211 | 77 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
212 | 82 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑔 ∈ 𝑉) |
213 | 14, 1, 17, 211, 81, 212, 122, 192, 20 | frlmvscaval 19929 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘( ·𝑠
‘𝑌)𝑔)‘𝑥) = (𝑘 · (𝑔‘𝑥))) |
214 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
215 | 209, 210,
77, 77, 55, 213, 214 | offval 6802 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔) ∘𝑓
(+g‘𝑅)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))) |
216 | 204, 215 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))) |
217 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) ∈ V |
218 | 217 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) ∈ V) |
219 | 216, 218 | fvmpt2d 6202 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) = ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥))) |
220 | 219 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥))) |
221 | 17, 75, 20 | ringdir 18390 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ ((𝑘 · (𝑔‘𝑥)) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
222 | 79, 109, 99, 91, 221 | syl13anc 1320 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
223 | 129 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
224 | 220, 222,
223 | 3eqtrd 2648 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
225 | 224 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) |
226 | 225 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
227 | 203, 226 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
228 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑒 = 𝑔) |
229 | 228 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (𝑔‘𝑥)) |
230 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
231 | 230 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
232 | 229, 231 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑖‘𝑥))) |
233 | 232 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
234 | 233 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
235 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) ∈ V |
236 | 235 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
237 | 179, 234,
83, 88, 236 | ovmpt2d 6686 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑔 , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
238 | 237 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
239 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 19938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
240 | 154, 82, 86, 239 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
241 | 17, 24, 75, 20, 78, 77, 80, 93, 240 | gsummulc2 18430 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
242 | 238, 241 | eqtr4d 2647 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
243 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑒 = ℎ) |
244 | 243 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (ℎ‘𝑥)) |
245 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
246 | 245 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
247 | 244, 246 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑖‘𝑥))) |
248 | 247 | mpteq2dv 4673 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) |
249 | 248 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))) |
250 | | ovex 6577 |
. . . . . 6
⊢ (𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) ∈ V |
251 | 250 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
252 | 179, 249,
97, 88, 251 | ovmpt2d 6686 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (ℎ , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))) |
253 | 242, 252 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖)) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
254 | 165, 227,
253 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖))) |
255 | 34 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CRing) |
256 | 255 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) |
257 | 17, 20 | crngcom 18385 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
258 | 256, 66, 65, 257 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
259 | 258 | mpteq2dva 4672 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
260 | 259 | oveq2d 6565 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
261 | 178 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → , = (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
262 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑒 = ℎ) |
263 | 262 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑒‘𝑥) = (ℎ‘𝑥)) |
264 | | simprr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑓 = 𝑔) |
265 | 264 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑓‘𝑥) = (𝑔‘𝑥)) |
266 | 263, 265 | oveq12d 6567 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑔‘𝑥))) |
267 | 266 | mpteq2dv 4673 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) |
268 | 267 | oveq2d 6565 |
. . . 4
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) |
269 | | ovex 6577 |
. . . . 5
⊢ (𝑅 Σg
(𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) ∈ V |
270 | 269 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) ∈ V) |
271 | 261, 268,
50, 44, 270 | ovmpt2d 6686 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (ℎ , 𝑔) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) |
272 | 35 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
273 | 272 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
274 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑔 , ℎ) → ( ∗ ‘𝑥) = ( ∗ ‘(𝑔 , ℎ))) |
275 | | id 22 |
. . . . . . 7
⊢ (𝑥 = (𝑔 , ℎ) → 𝑥 = (𝑔 , ℎ)) |
276 | 274, 275 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 = (𝑔 , ℎ) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ))) |
277 | 276 | rspcv 3278 |
. . . . 5
⊢ ((𝑔 , ℎ) ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥 → ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ))) |
278 | 74, 273, 277 | sylc 63 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ)) |
279 | 278, 60 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
280 | 260, 271,
279 | 3eqtr4rd 2655 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (ℎ , 𝑔)) |
281 | 2, 3, 4, 6, 8, 16,
18, 19, 21, 23, 25, 33, 36, 74, 254, 71, 280 | isphld 19818 |
1
⊢ (𝜑 → 𝑌 ∈ PreHil) |