Step | Hyp | Ref
| Expression |
1 | | frlmphl.v |
. . 3
⊢ 𝑉 = (Base‘𝑌) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝑉 = (Base‘𝑌)) |
3 | | eqidd 2652 |
. 2
⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌)) |
4 | | eqidd 2652 |
. 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 18804 |
. . . . 5
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
11 | 9, 10 | sylib 208 |
. . . 4
⊢ (𝜑 → (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
12 | 11 | simpld 474 |
. . 3
⊢ (𝜑 → 𝑅 ∈ DivRing) |
13 | | frlmphl.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
14 | | frlmphl.y |
. . . 4
⊢ 𝑌 = (𝑅 freeLMod 𝐼) |
15 | 14 | frlmsca 20145 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊) → 𝑅 = (Scalar‘𝑌)) |
16 | 12, 13, 15 | syl2anc 694 |
. 2
⊢ (𝜑 → 𝑅 = (Scalar‘𝑌)) |
17 | | frlmphl.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
18 | 17 | a1i 11 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
19 | | eqidd 2652 |
. 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 18802 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
27 | 12, 26 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
28 | 14 | frlmlmod 20141 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ LMod) |
29 | 27, 13, 28 | syl2anc 694 |
. . 3
⊢ (𝜑 → 𝑌 ∈ LMod) |
30 | 16, 12 | eqeltrrd 2731 |
. . 3
⊢ (𝜑 → (Scalar‘𝑌) ∈
DivRing) |
31 | | eqid 2651 |
. . . 4
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
32 | 31 | islvec 19152 |
. . 3
⊢ (𝑌 ∈ LVec ↔ (𝑌 ∈ LMod ∧
(Scalar‘𝑌) ∈
DivRing)) |
33 | 29, 30, 32 | sylanbrc 699 |
. 2
⊢ (𝜑 → 𝑌 ∈ LVec) |
34 | 11 | simprd 478 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
35 | | frlmphl.u |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥) |
36 | 17, 22, 34, 35 | idsrngd 18910 |
. 2
⊢ (𝜑 → 𝑅 ∈ *-Ring) |
37 | 13 | 3ad2ant1 1102 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝐼 ∈ 𝑊) |
38 | 27 | 3ad2ant1 1102 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ Ring) |
39 | | simp2 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ 𝑉) |
40 | | simp3 1083 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ 𝑉) |
41 | 14, 17, 20, 1, 5 | frlmipval 20166 |
. . . . 5
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉)) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘𝑓
·
ℎ))) |
42 | 37, 38, 39, 40, 41 | syl22anc 1367 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘𝑓
·
ℎ))) |
43 | 14, 17, 1 | frlmbasmap 20151 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) |
44 | 37, 39, 43 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) |
45 | | elmapi 7921 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) → 𝑔:𝐼⟶𝐵) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔:𝐼⟶𝐵) |
47 | | ffn 6083 |
. . . . . . 7
⊢ (𝑔:𝐼⟶𝐵 → 𝑔 Fn 𝐼) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 Fn 𝐼) |
49 | 14, 17, 1 | frlmbasmap 20151 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑𝑚 𝐼)) |
50 | 37, 40, 49 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑𝑚 𝐼)) |
51 | | elmapi 7921 |
. . . . . . . 8
⊢ (ℎ ∈ (𝐵 ↑𝑚 𝐼) → ℎ:𝐼⟶𝐵) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ:𝐼⟶𝐵) |
53 | | ffn 6083 |
. . . . . . 7
⊢ (ℎ:𝐼⟶𝐵 → ℎ Fn 𝐼) |
54 | 52, 53 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ Fn 𝐼) |
55 | | inidm 3855 |
. . . . . 6
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
56 | | eqidd 2652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
57 | | eqidd 2652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
58 | 48, 54, 37, 37, 55, 56, 57 | offval 6946 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 ∘𝑓 · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
59 | 58 | oveq2d 6706 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑔 ∘𝑓
·
ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
60 | 42, 59 | eqtrd 2685 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
61 | | ringcmn 18627 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
62 | 27, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
63 | 62 | 3ad2ant1 1102 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CMnd) |
64 | 38 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
65 | 46 | ffvelrnda 6399 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵) |
66 | 52 | ffvelrnda 6399 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵) |
67 | 17, 20 | ringcl 18607 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵) |
68 | 64, 65, 66, 67 | syl3anc 1366 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵) |
69 | | eqid 2651 |
. . . . 5
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) |
70 | 68, 69 | fmptd 6425 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))):𝐼⟶𝐵) |
71 | | frlmphl.m |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) |
72 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 20167 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 ) |
73 | 17, 24, 63, 37, 70, 72 | gsumcl 18362 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) ∈ 𝐵) |
74 | 60, 73 | eqeltrd 2730 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) ∈ 𝐵) |
75 | | eqid 2651 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
76 | 62 | 3ad2ant1 1102 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ CMnd) |
77 | 13 | 3ad2ant1 1102 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐼 ∈ 𝑊) |
78 | 27 | 3ad2ant1 1102 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ Ring) |
79 | 78 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
80 | | simp2 1082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ 𝐵) |
81 | 80 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑘 ∈ 𝐵) |
82 | | simp31 1117 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ 𝑉) |
83 | 77, 82, 43 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ (𝐵 ↑𝑚 𝐼)) |
84 | 83, 45 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔:𝐼⟶𝐵) |
85 | 84 | ffvelrnda 6399 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵) |
86 | | simp33 1119 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ 𝑉) |
87 | 14, 17, 1 | frlmbasmap 20151 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ (𝐵 ↑𝑚 𝐼)) |
88 | 77, 86, 87 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ (𝐵 ↑𝑚 𝐼)) |
89 | | elmapi 7921 |
. . . . . . . 8
⊢ (𝑖 ∈ (𝐵 ↑𝑚 𝐼) → 𝑖:𝐼⟶𝐵) |
90 | 88, 89 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖:𝐼⟶𝐵) |
91 | 90 | ffvelrnda 6399 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) ∈ 𝐵) |
92 | 17, 20 | ringcl 18607 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
93 | 79, 85, 91, 92 | syl3anc 1366 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
94 | 17, 20 | ringcl 18607 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵) |
95 | 79, 81, 93, 94 | syl3anc 1366 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵) |
96 | | simp32 1118 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ 𝑉) |
97 | 77, 96, 49 | syl2anc 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ (𝐵 ↑𝑚 𝐼)) |
98 | 97, 51 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ:𝐼⟶𝐵) |
99 | 98 | ffvelrnda 6399 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵) |
100 | 17, 20 | ringcl 18607 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
101 | 79, 99, 91, 100 | syl3anc 1366 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
102 | | eqidd 2652 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
103 | | eqidd 2652 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) |
104 | | fveq2 6229 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦)) |
105 | 104 | oveq2d 6706 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑘 · (𝑔‘𝑥)) = (𝑘 · (𝑔‘𝑦))) |
106 | 105 | cbvmptv 4783 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) |
107 | 106 | oveq1i 6700 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) = ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘𝑓 · 𝑖) |
108 | 17, 20 | ringcl 18607 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵) |
109 | 79, 81, 85, 108 | syl3anc 1366 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵) |
110 | | eqid 2651 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) |
111 | 109, 110 | fmptd 6425 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))):𝐼⟶𝐵) |
112 | | ffn 6083 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))):𝐼⟶𝐵 → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼) |
113 | 111, 112 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼) |
114 | 106 | fneq1i 6023 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼 ↔ (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼) |
115 | 113, 114 | sylib 208 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼) |
116 | | ffn 6083 |
. . . . . . . . 9
⊢ (𝑖:𝐼⟶𝐵 → 𝑖 Fn 𝐼) |
117 | 90, 116 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 Fn 𝐼) |
118 | | eqidd 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))) |
119 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
120 | 119 | fveq2d 6233 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑔‘𝑦) = (𝑔‘𝑥)) |
121 | 120 | oveq2d 6706 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑘 · (𝑔‘𝑦)) = (𝑘 · (𝑔‘𝑥))) |
122 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
123 | | ovexd 6720 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ V) |
124 | 118, 121,
122, 123 | fvmptd 6327 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))‘𝑥) = (𝑘 · (𝑔‘𝑥))) |
125 | | eqidd 2652 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) = (𝑖‘𝑥)) |
126 | 115, 117,
77, 77, 55, 124, 125 | offval 6946 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘𝑓 · 𝑖) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)))) |
127 | 17, 20 | ringass 18610 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
128 | 79, 81, 85, 91, 127 | syl13anc 1368 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
129 | 128 | mpteq2dva 4777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
130 | 126, 129 | eqtrd 2685 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘𝑓 · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
131 | 107, 130 | syl5eq 2697 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
132 | | ovexd 6720 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ∈ V) |
133 | | funmpt 5964 |
. . . . . . 7
⊢ Fun
(𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧))) |
134 | | eqidd 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑧 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) = ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧)) |
135 | | eqidd 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑧 ∈ 𝐼) → (𝑖‘𝑧) = (𝑖‘𝑧)) |
136 | 113, 117,
77, 77, 55, 134, 135 | offval 6946 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) = (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧)))) |
137 | 136 | funeqd 5948 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ↔ Fun (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧))))) |
138 | 133, 137 | mpbiri 248 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖)) |
139 | | simp3 1083 |
. . . . . . . . 9
⊢ ((𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ 𝑉) |
140 | 13, 139 | anim12i 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉)) |
141 | 140 | 3adant2 1100 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉)) |
142 | 14, 24, 1 | frlmbasfsupp 20150 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 finSupp 0 ) |
143 | 141, 142 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 finSupp 0 ) |
144 | 17, 24 | ring0cl 18615 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
145 | 78, 144 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 0 ∈ 𝐵) |
146 | 17, 20, 24 | ringrz 18634 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 ) |
147 | 78, 146 | sylan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 ) |
148 | 77, 145, 111, 90, 147 | suppofss2d 7378 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 )) |
149 | | fsuppsssupp 8332 |
. . . . . 6
⊢
(((((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) ∈ V ∧ Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖)) ∧ (𝑖 finSupp 0 ∧ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) finSupp 0 ) |
150 | 132, 138,
143, 148, 149 | syl22anc 1367 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘𝑓 · 𝑖) finSupp 0 ) |
151 | 131, 150 | eqbrtrrd 4709 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) finSupp 0 ) |
152 | | simp1 1081 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝜑) |
153 | | eleq1 2718 |
. . . . . . . . 9
⊢ (𝑔 = ℎ → (𝑔 ∈ 𝑉 ↔ ℎ ∈ 𝑉)) |
154 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑔 = ℎ → 𝑔 = ℎ) |
155 | 154, 154 | oveq12d 6708 |
. . . . . . . . . 10
⊢ (𝑔 = ℎ → (𝑔 , 𝑔) = (ℎ , ℎ)) |
156 | 155 | eqeq1d 2653 |
. . . . . . . . 9
⊢ (𝑔 = ℎ → ((𝑔 , 𝑔) = 0 ↔ (ℎ , ℎ) = 0 )) |
157 | 153, 156 | 3anbi23d 1442 |
. . . . . . . 8
⊢ (𝑔 = ℎ → ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) ↔ (𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ))) |
158 | | eqeq1 2655 |
. . . . . . . 8
⊢ (𝑔 = ℎ → (𝑔 = 𝑂 ↔ ℎ = 𝑂)) |
159 | 157, 158 | imbi12d 333 |
. . . . . . 7
⊢ (𝑔 = ℎ → (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) ↔ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂))) |
160 | 159, 71 | chvarv 2299 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂) |
161 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 160, 35, 13 | frlmphllem 20167 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
162 | 152, 96, 86, 161 | syl3anc 1366 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
163 | 17, 24, 75, 76, 77, 95, 101, 102, 103, 151, 162 | gsummptfsadd 18370 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
164 | 14, 17, 20 | frlmip 20165 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ DivRing) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) =
(·𝑖‘𝑌)) |
165 | 13, 12, 164 | syl2anc 694 |
. . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) =
(·𝑖‘𝑌)) |
166 | 165, 5 | syl6reqr 2704 |
. . . . . . 7
⊢ (𝜑 → , = (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))) |
167 | | fveq1 6228 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑔 → (𝑒‘𝑥) = (𝑔‘𝑥)) |
168 | 167 | oveq1d 6705 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑔 → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑓‘𝑥))) |
169 | 168 | mpteq2dv 4778 |
. . . . . . . . 9
⊢ (𝑒 = 𝑔 → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) |
170 | 169 | oveq2d 6706 |
. . . . . . . 8
⊢ (𝑒 = 𝑔 → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))))) |
171 | | fveq1 6228 |
. . . . . . . . . . 11
⊢ (𝑓 = ℎ → (𝑓‘𝑥) = (ℎ‘𝑥)) |
172 | 171 | oveq2d 6706 |
. . . . . . . . . 10
⊢ (𝑓 = ℎ → ((𝑔‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
173 | 172 | mpteq2dv 4778 |
. . . . . . . . 9
⊢ (𝑓 = ℎ → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
174 | 173 | oveq2d 6706 |
. . . . . . . 8
⊢ (𝑓 = ℎ → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
175 | 170, 174 | cbvmpt2v 6777 |
. . . . . . 7
⊢ (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼), ℎ ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
176 | 166, 175 | syl6eqr 2703 |
. . . . . 6
⊢ (𝜑 → , = (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
177 | 176 | 3ad2ant1 1102 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → , = (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
178 | | simprl 809 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)) |
179 | 178 | fveq1d 6231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥)) |
180 | | simprr 811 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
181 | 180 | fveq1d 6231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
182 | 179, 181 | oveq12d 6708 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) |
183 | 182 | mpteq2dv 4778 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) |
184 | 183 | oveq2d 6706 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))) |
185 | 29 | 3ad2ant1 1102 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑌 ∈ LMod) |
186 | 16 | 3ad2ant1 1102 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 = (Scalar‘𝑌)) |
187 | 186 | fveq2d 6233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Base‘𝑅) = (Base‘(Scalar‘𝑌))) |
188 | 17, 187 | syl5eq 2697 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐵 = (Base‘(Scalar‘𝑌))) |
189 | 80, 188 | eleqtrd 2732 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ (Base‘(Scalar‘𝑌))) |
190 | | eqid 2651 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
191 | | eqid 2651 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
192 | 1, 31, 190, 191 | lmodvscl 18928 |
. . . . . . . 8
⊢ ((𝑌 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑔 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) |
193 | 185, 189,
82, 192 | syl3anc 1366 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) |
194 | | eqid 2651 |
. . . . . . . 8
⊢
(+g‘𝑌) = (+g‘𝑌) |
195 | 1, 194 | lmodvacl 18925 |
. . . . . . 7
⊢ ((𝑌 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑌)𝑔) ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) |
196 | 185, 193,
96, 195 | syl3anc 1366 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) |
197 | 14, 17, 1 | frlmbasmap 20151 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑𝑚 𝐼)) |
198 | 77, 196, 197 | syl2anc 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑𝑚 𝐼)) |
199 | | ovexd 6720 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
200 | 177, 184,
198, 88, 199 | ovmpt2d 6830 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))) |
201 | 14, 1, 78, 77, 193, 96, 75, 194 | frlmplusgval 20155 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) = ((𝑘( ·𝑠
‘𝑌)𝑔) ∘𝑓
(+g‘𝑅)ℎ)) |
202 | 14, 17, 1 | frlmbasmap 20151 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ (𝐵 ↑𝑚 𝐼)) |
203 | 77, 193, 202 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ (𝐵 ↑𝑚 𝐼)) |
204 | | elmapi 7921 |
. . . . . . . . . . . 12
⊢ ((𝑘(
·𝑠 ‘𝑌)𝑔) ∈ (𝐵 ↑𝑚 𝐼) → (𝑘( ·𝑠
‘𝑌)𝑔):𝐼⟶𝐵) |
205 | | ffn 6083 |
. . . . . . . . . . . 12
⊢ ((𝑘(
·𝑠 ‘𝑌)𝑔):𝐼⟶𝐵 → (𝑘( ·𝑠
‘𝑌)𝑔) Fn 𝐼) |
206 | 203, 204,
205 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) Fn 𝐼) |
207 | 98, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ Fn 𝐼) |
208 | 77 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
209 | 82 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑔 ∈ 𝑉) |
210 | 14, 1, 17, 208, 81, 209, 122, 190, 20 | frlmvscaval 20158 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘( ·𝑠
‘𝑌)𝑔)‘𝑥) = (𝑘 · (𝑔‘𝑥))) |
211 | | eqidd 2652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
212 | 206, 207,
77, 77, 55, 210, 211 | offval 6946 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔) ∘𝑓
(+g‘𝑅)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))) |
213 | 201, 212 | eqtrd 2685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))) |
214 | | ovexd 6720 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) ∈ V) |
215 | 213, 214 | fvmpt2d 6332 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) = ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥))) |
216 | 215 | oveq1d 6705 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥))) |
217 | 17, 75, 20 | ringdir 18613 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ ((𝑘 · (𝑔‘𝑥)) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
218 | 79, 109, 99, 91, 217 | syl13anc 1368 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
219 | 128 | oveq1d 6705 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
220 | 216, 218,
219 | 3eqtrd 2689 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
221 | 220 | mpteq2dva 4777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) |
222 | 221 | oveq2d 6706 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
223 | 200, 222 | eqtrd 2685 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
224 | | simprl 809 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑒 = 𝑔) |
225 | 224 | fveq1d 6231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (𝑔‘𝑥)) |
226 | | simprr 811 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
227 | 226 | fveq1d 6231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
228 | 225, 227 | oveq12d 6708 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑖‘𝑥))) |
229 | 228 | mpteq2dv 4778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
230 | 229 | oveq2d 6706 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
231 | | ovexd 6720 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
232 | 177, 230,
83, 88, 231 | ovmpt2d 6830 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑔 , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
233 | 232 | oveq2d 6706 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
234 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 20167 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
235 | 152, 82, 86, 234 | syl3anc 1366 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
236 | 17, 24, 75, 20, 78, 77, 80, 93, 235 | gsummulc2 18653 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
237 | 233, 236 | eqtr4d 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
238 | | simprl 809 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑒 = ℎ) |
239 | 238 | fveq1d 6231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (ℎ‘𝑥)) |
240 | | simprr 811 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
241 | 240 | fveq1d 6231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
242 | 239, 241 | oveq12d 6708 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑖‘𝑥))) |
243 | 242 | mpteq2dv 4778 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) |
244 | 243 | oveq2d 6706 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))) |
245 | | ovexd 6720 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
246 | 177, 244,
97, 88, 245 | ovmpt2d 6830 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (ℎ , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))) |
247 | 237, 246 | oveq12d 6708 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖)) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
248 | 163, 223,
247 | 3eqtr4d 2695 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖))) |
249 | 34 | 3ad2ant1 1102 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CRing) |
250 | 249 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) |
251 | 17, 20 | crngcom 18608 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
252 | 250, 66, 65, 251 | syl3anc 1366 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
253 | 252 | mpteq2dva 4777 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
254 | 253 | oveq2d 6706 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
255 | 176 | 3ad2ant1 1102 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → , = (𝑒 ∈ (𝐵 ↑𝑚 𝐼), 𝑓 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
256 | | simprl 809 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑒 = ℎ) |
257 | 256 | fveq1d 6231 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑒‘𝑥) = (ℎ‘𝑥)) |
258 | | simprr 811 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑓 = 𝑔) |
259 | 258 | fveq1d 6231 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑓‘𝑥) = (𝑔‘𝑥)) |
260 | 257, 259 | oveq12d 6708 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑔‘𝑥))) |
261 | 260 | mpteq2dv 4778 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) |
262 | 261 | oveq2d 6706 |
. . . 4
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) |
263 | | ovexd 6720 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) ∈ V) |
264 | 255, 262,
50, 44, 263 | ovmpt2d 6830 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (ℎ , 𝑔) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) |
265 | 35 | ralrimiva 2995 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
266 | 265 | 3ad2ant1 1102 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
267 | | fveq2 6229 |
. . . . . . 7
⊢ (𝑥 = (𝑔 , ℎ) → ( ∗ ‘𝑥) = ( ∗ ‘(𝑔 , ℎ))) |
268 | | id 22 |
. . . . . . 7
⊢ (𝑥 = (𝑔 , ℎ) → 𝑥 = (𝑔 , ℎ)) |
269 | 267, 268 | eqeq12d 2666 |
. . . . . 6
⊢ (𝑥 = (𝑔 , ℎ) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ))) |
270 | 269 | rspcv 3336 |
. . . . 5
⊢ ((𝑔 , ℎ) ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥 → ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ))) |
271 | 74, 266, 270 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ)) |
272 | 271, 60 | eqtrd 2685 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
273 | 254, 264,
272 | 3eqtr4rd 2696 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (ℎ , 𝑔)) |
274 | 2, 3, 4, 6, 8, 16,
18, 19, 21, 23, 25, 33, 36, 74, 248, 71, 273 | isphld 20047 |
1
⊢ (𝜑 → 𝑌 ∈ PreHil) |