| Step | Hyp | Ref
| Expression |
| 1 | | frlmphl.v |
. . 3
⊢ 𝑉 = (Base‘𝑌) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝑉 = (Base‘𝑌)) |
| 3 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌)) |
| 4 | | eqidd 2738 |
. 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 20740 |
. . . . 5
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
| 11 | 9, 10 | sylib 218 |
. . . 4
⊢ (𝜑 → (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
| 12 | 11 | simpld 494 |
. . 3
⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 13 | | frlmphl.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
| 14 | | frlmphl.y |
. . . 4
⊢ 𝑌 = (𝑅 freeLMod 𝐼) |
| 15 | 14 | frlmsca 21773 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊) → 𝑅 = (Scalar‘𝑌)) |
| 16 | 12, 13, 15 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑅 = (Scalar‘𝑌)) |
| 17 | | frlmphl.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
| 18 | 17 | a1i 11 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
| 19 | | eqidd 2738 |
. 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 | 12 | drngringd 20737 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 27 | 14 | frlmlmod 21769 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ LMod) |
| 28 | 26, 13, 27 | syl2anc 584 |
. . 3
⊢ (𝜑 → 𝑌 ∈ LMod) |
| 29 | 16, 12 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → (Scalar‘𝑌) ∈
DivRing) |
| 30 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
| 31 | 30 | islvec 21103 |
. . 3
⊢ (𝑌 ∈ LVec ↔ (𝑌 ∈ LMod ∧
(Scalar‘𝑌) ∈
DivRing)) |
| 32 | 28, 29, 31 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝑌 ∈ LVec) |
| 33 | 9 | fldcrngd 20742 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 34 | | frlmphl.u |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥) |
| 35 | 17, 22, 33, 34 | idsrngd 20857 |
. 2
⊢ (𝜑 → 𝑅 ∈ *-Ring) |
| 36 | 13 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝐼 ∈ 𝑊) |
| 37 | 26 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ Ring) |
| 38 | | simp2 1138 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ 𝑉) |
| 39 | | simp3 1139 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ 𝑉) |
| 40 | 14, 17, 20, 1, 5 | frlmipval 21799 |
. . . . 5
⊢ (((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉)) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘f · ℎ))) |
| 41 | 36, 37, 38, 39, 40 | syl22anc 839 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘f · ℎ))) |
| 42 | 14, 17, 1 | frlmbasmap 21779 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑m 𝐼)) |
| 43 | 36, 38, 42 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑m 𝐼)) |
| 44 | | elmapi 8889 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) → 𝑔:𝐼⟶𝐵) |
| 45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔:𝐼⟶𝐵) |
| 46 | 45 | ffnd 6737 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 Fn 𝐼) |
| 47 | 14, 17, 1 | frlmbasmap 21779 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑m 𝐼)) |
| 48 | 36, 39, 47 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑m 𝐼)) |
| 49 | | elmapi 8889 |
. . . . . . . 8
⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ:𝐼⟶𝐵) |
| 50 | 48, 49 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ:𝐼⟶𝐵) |
| 51 | 50 | ffnd 6737 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ Fn 𝐼) |
| 52 | | inidm 4227 |
. . . . . 6
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
| 53 | | eqidd 2738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
| 54 | | eqidd 2738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
| 55 | 46, 51, 36, 36, 52, 53, 54 | offval 7706 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 ∘f · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
| 56 | 55 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑔 ∘f · ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 57 | 41, 56 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 58 | 26 | ringcmnd 20281 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 59 | 58 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CMnd) |
| 60 | 37 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
| 61 | 45 | ffvelcdmda 7104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵) |
| 62 | 50 | ffvelcdmda 7104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵) |
| 63 | 17, 20, 60, 61, 62 | ringcld 20257 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵) |
| 64 | 63 | fmpttd 7135 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))):𝐼⟶𝐵) |
| 65 | | frlmphl.m |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) |
| 66 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 65, 34, 13 | frlmphllem 21800 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 ) |
| 67 | 17, 24, 59, 36, 64, 66 | gsumcl 19933 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) ∈ 𝐵) |
| 68 | 57, 67 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) ∈ 𝐵) |
| 69 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 70 | 58 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ CMnd) |
| 71 | 13 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐼 ∈ 𝑊) |
| 72 | 26 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ Ring) |
| 73 | 72 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
| 74 | | simp2 1138 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ 𝐵) |
| 75 | 74 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑘 ∈ 𝐵) |
| 76 | | simp31 1210 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ 𝑉) |
| 77 | 71, 76, 42 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ (𝐵 ↑m 𝐼)) |
| 78 | 77, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔:𝐼⟶𝐵) |
| 79 | 78 | ffvelcdmda 7104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵) |
| 80 | | simp33 1212 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ 𝑉) |
| 81 | 14, 17, 1 | frlmbasmap 21779 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ (𝐵 ↑m 𝐼)) |
| 82 | 71, 80, 81 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ (𝐵 ↑m 𝐼)) |
| 83 | | elmapi 8889 |
. . . . . . . 8
⊢ (𝑖 ∈ (𝐵 ↑m 𝐼) → 𝑖:𝐼⟶𝐵) |
| 84 | 82, 83 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖:𝐼⟶𝐵) |
| 85 | 84 | ffvelcdmda 7104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) ∈ 𝐵) |
| 86 | 17, 20, 73, 79, 85 | ringcld 20257 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
| 87 | 17, 20, 73, 75, 86 | ringcld 20257 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵) |
| 88 | | simp32 1211 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ 𝑉) |
| 89 | 71, 88, 47 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ (𝐵 ↑m 𝐼)) |
| 90 | 89, 49 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ:𝐼⟶𝐵) |
| 91 | 90 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵) |
| 92 | 17, 20, 73, 91, 85 | ringcld 20257 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) |
| 93 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
| 94 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) |
| 95 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦)) |
| 96 | 95 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑘 · (𝑔‘𝑥)) = (𝑘 · (𝑔‘𝑦))) |
| 97 | 96 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) |
| 98 | 97 | oveq1i 7441 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) = ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘f · 𝑖) |
| 99 | 17, 20, 73, 75, 79 | ringcld 20257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵) |
| 100 | 99 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))):𝐼⟶𝐵) |
| 101 | 100 | ffnd 6737 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼) |
| 102 | 97 | fneq1i 6665 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼 ↔ (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼) |
| 103 | 101, 102 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼) |
| 104 | 84 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 Fn 𝐼) |
| 105 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))) |
| 106 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
| 107 | 106 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑔‘𝑦) = (𝑔‘𝑥)) |
| 108 | 107 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑘 · (𝑔‘𝑦)) = (𝑘 · (𝑔‘𝑥))) |
| 109 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
| 110 | | ovexd 7466 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ V) |
| 111 | 105, 108,
109, 110 | fvmptd 7023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))‘𝑥) = (𝑘 · (𝑔‘𝑥))) |
| 112 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) = (𝑖‘𝑥)) |
| 113 | 103, 104,
71, 71, 52, 111, 112 | offval 7706 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘f · 𝑖) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)))) |
| 114 | 17, 20 | ringass 20250 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
| 115 | 73, 75, 79, 85, 114 | syl13anc 1374 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
| 116 | 115 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
| 117 | 113, 116 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘f · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
| 118 | 98, 117 | eqtrid 2789 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
| 119 | | ovexd 7466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) ∈ V) |
| 120 | 101, 104,
71, 71 | offun 7711 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖)) |
| 121 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ 𝑉) |
| 122 | 13, 121 | anim12i 613 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉)) |
| 123 | 122 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉)) |
| 124 | 14, 24, 1 | frlmbasfsupp 21778 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 finSupp 0 ) |
| 125 | 123, 124 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 finSupp 0 ) |
| 126 | 17, 24 | ring0cl 20264 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
| 127 | 72, 126 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 0 ∈ 𝐵) |
| 128 | 17, 20, 24 | ringrz 20291 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 ) |
| 129 | 72, 128 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 ) |
| 130 | 71, 127, 100, 84, 129 | suppofss2d 8230 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 )) |
| 131 | | fsuppsssupp 9421 |
. . . . . 6
⊢
(((((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) ∈ V ∧ Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖)) ∧ (𝑖 finSupp 0 ∧ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) finSupp 0 ) |
| 132 | 119, 120,
125, 130, 131 | syl22anc 839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) finSupp 0 ) |
| 133 | 118, 132 | eqbrtrrd 5167 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) finSupp 0 ) |
| 134 | | simp1 1137 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝜑) |
| 135 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑔 = ℎ → (𝑔 ∈ 𝑉 ↔ ℎ ∈ 𝑉)) |
| 136 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑔 = ℎ → 𝑔 = ℎ) |
| 137 | 136, 136 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑔 = ℎ → (𝑔 , 𝑔) = (ℎ , ℎ)) |
| 138 | 137 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑔 = ℎ → ((𝑔 , 𝑔) = 0 ↔ (ℎ , ℎ) = 0 )) |
| 139 | 135, 138 | 3anbi23d 1441 |
. . . . . . . 8
⊢ (𝑔 = ℎ → ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) ↔ (𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ))) |
| 140 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑔 = ℎ → (𝑔 = 𝑂 ↔ ℎ = 𝑂)) |
| 141 | 139, 140 | imbi12d 344 |
. . . . . . 7
⊢ (𝑔 = ℎ → (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) ↔ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂))) |
| 142 | 141, 65 | chvarvv 1998 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂) |
| 143 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 142, 34, 13 | frlmphllem 21800 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
| 144 | 134, 88, 80, 143 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
| 145 | 17, 24, 69, 70, 71, 87, 92, 93, 94, 133, 144 | gsummptfsadd 19942 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
| 146 | 14, 17, 20 | frlmip 21798 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ DivRing) → (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) =
(·𝑖‘𝑌)) |
| 147 | 13, 12, 146 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) =
(·𝑖‘𝑌)) |
| 148 | 5, 147 | eqtr4id 2796 |
. . . . . . 7
⊢ (𝜑 → , = (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))) |
| 149 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑔 → (𝑒‘𝑥) = (𝑔‘𝑥)) |
| 150 | 149 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑔 → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑓‘𝑥))) |
| 151 | 150 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (𝑒 = 𝑔 → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) |
| 152 | 151 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑒 = 𝑔 → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))))) |
| 153 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑓 = ℎ → (𝑓‘𝑥) = (ℎ‘𝑥)) |
| 154 | 153 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑓 = ℎ → ((𝑔‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
| 155 | 154 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (𝑓 = ℎ → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
| 156 | 155 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑓 = ℎ → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 157 | 152, 156 | cbvmpov 7528 |
. . . . . . 7
⊢ (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))) = (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 158 | 148, 157 | eqtr4di 2795 |
. . . . . 6
⊢ (𝜑 → , = (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
| 159 | 158 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → , = (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
| 160 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)) |
| 161 | 160 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥)) |
| 162 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
| 163 | 162 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
| 164 | 161, 163 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) |
| 165 | 164 | mpteq2dv 5244 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) |
| 166 | 165 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))) |
| 167 | 28 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑌 ∈ LMod) |
| 168 | 16 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 = (Scalar‘𝑌)) |
| 169 | 168 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Base‘𝑅) = (Base‘(Scalar‘𝑌))) |
| 170 | 17, 169 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐵 = (Base‘(Scalar‘𝑌))) |
| 171 | 74, 170 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ (Base‘(Scalar‘𝑌))) |
| 172 | | eqid 2737 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
| 173 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
| 174 | 1, 30, 172, 173 | lmodvscl 20876 |
. . . . . . . 8
⊢ ((𝑌 ∈ LMod ∧ 𝑘 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑔 ∈ 𝑉) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) |
| 175 | 167, 171,
76, 174 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) |
| 176 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑌) = (+g‘𝑌) |
| 177 | 1, 176 | lmodvacl 20873 |
. . . . . . 7
⊢ ((𝑌 ∈ LMod ∧ (𝑘(
·𝑠 ‘𝑌)𝑔) ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) |
| 178 | 167, 175,
88, 177 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) |
| 179 | 14, 17, 1 | frlmbasmap 21779 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑊 ∧ ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑m 𝐼)) |
| 180 | 71, 178, 179 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑m 𝐼)) |
| 181 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
| 182 | 159, 166,
180, 82, 181 | ovmpod 7585 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))) |
| 183 | 14, 1, 72, 71, 175, 88, 69, 176 | frlmplusgval 21784 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) = ((𝑘( ·𝑠
‘𝑌)𝑔) ∘f
(+g‘𝑅)ℎ)) |
| 184 | 14, 17, 1 | frlmbasmap 21779 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ (𝑘( ·𝑠
‘𝑌)𝑔) ∈ 𝑉) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ (𝐵 ↑m 𝐼)) |
| 185 | 71, 175, 184 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) ∈ (𝐵 ↑m 𝐼)) |
| 186 | | elmapi 8889 |
. . . . . . . . . . . 12
⊢ ((𝑘(
·𝑠 ‘𝑌)𝑔) ∈ (𝐵 ↑m 𝐼) → (𝑘( ·𝑠
‘𝑌)𝑔):𝐼⟶𝐵) |
| 187 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ ((𝑘(
·𝑠 ‘𝑌)𝑔):𝐼⟶𝐵 → (𝑘( ·𝑠
‘𝑌)𝑔) Fn 𝐼) |
| 188 | 185, 186,
187 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠
‘𝑌)𝑔) Fn 𝐼) |
| 189 | 90 | ffnd 6737 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ Fn 𝐼) |
| 190 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
| 191 | 76 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑔 ∈ 𝑉) |
| 192 | 14, 1, 17, 190, 75, 191, 109, 172, 20 | frlmvscaval 21788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘( ·𝑠
‘𝑌)𝑔)‘𝑥) = (𝑘 · (𝑔‘𝑥))) |
| 193 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
| 194 | 188, 189,
71, 71, 52, 192, 193 | offval 7706 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔) ∘f
(+g‘𝑅)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))) |
| 195 | 183, 194 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))) |
| 196 | | ovexd 7466 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) ∈ V) |
| 197 | 195, 196 | fvmpt2d 7029 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) = ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥))) |
| 198 | 197 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥))) |
| 199 | 17, 69, 20 | ringdir 20259 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ ((𝑘 · (𝑔‘𝑥)) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
| 200 | 73, 99, 91, 85, 199 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
| 201 | 115 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
| 202 | 198, 200,
201 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))) |
| 203 | 202 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) |
| 204 | 203 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
| 205 | 182, 204 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
| 206 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑒 = 𝑔) |
| 207 | 206 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (𝑔‘𝑥)) |
| 208 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
| 209 | 208 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
| 210 | 207, 209 | oveq12d 7449 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑖‘𝑥))) |
| 211 | 210 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) |
| 212 | 211 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
| 213 | | ovexd 7466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
| 214 | 159, 212,
77, 82, 213 | ovmpod 7585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑔 , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))) |
| 215 | 214 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
| 216 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 65, 34, 13 | frlmphllem 21800 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
| 217 | 134, 76, 80, 216 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 ) |
| 218 | 17, 24, 20, 72, 71, 74, 86, 217 | gsummulc2 20314 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
| 219 | 215, 218 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))) |
| 220 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑒 = ℎ) |
| 221 | 220 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (ℎ‘𝑥)) |
| 222 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖) |
| 223 | 222 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥)) |
| 224 | 221, 223 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑖‘𝑥))) |
| 225 | 224 | mpteq2dv 5244 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) |
| 226 | 225 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))) |
| 227 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) ∈ V) |
| 228 | 159, 226,
89, 82, 227 | ovmpod 7585 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (ℎ , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))) |
| 229 | 219, 228 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖)) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))) |
| 230 | 145, 205,
229 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠
‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖))) |
| 231 | 33 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CRing) |
| 232 | 231 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) |
| 233 | 17, 20 | crngcom 20248 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
| 234 | 232, 62, 61, 233 | syl3anc 1373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥))) |
| 235 | 234 | mpteq2dva 5242 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
| 236 | 235 | oveq2d 7447 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 237 | 158 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → , = (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))))) |
| 238 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑒 = ℎ) |
| 239 | 238 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑒‘𝑥) = (ℎ‘𝑥)) |
| 240 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑓 = 𝑔) |
| 241 | 240 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑓‘𝑥) = (𝑔‘𝑥)) |
| 242 | 239, 241 | oveq12d 7449 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑔‘𝑥))) |
| 243 | 242 | mpteq2dv 5244 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) |
| 244 | 243 | oveq2d 7447 |
. . . 4
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) |
| 245 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) ∈ V) |
| 246 | 237, 244,
48, 43, 245 | ovmpod 7585 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (ℎ , 𝑔) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))) |
| 247 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (𝑔 , ℎ) → ( ∗ ‘𝑥) = ( ∗ ‘(𝑔 , ℎ))) |
| 248 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝑔 , ℎ) → 𝑥 = (𝑔 , ℎ)) |
| 249 | 247, 248 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = (𝑔 , ℎ) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ))) |
| 250 | 34 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
| 251 | 250 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥) |
| 252 | 249, 251,
68 | rspcdva 3623 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ)) |
| 253 | 252, 57 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 254 | 236, 246,
253 | 3eqtr4rd 2788 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (ℎ , 𝑔)) |
| 255 | 2, 3, 4, 6, 8, 16,
18, 19, 21, 23, 25, 32, 35, 68, 230, 65, 254 | isphld 21672 |
1
⊢ (𝜑 → 𝑌 ∈ PreHil) |