Proof of Theorem frlmphllem
| Step | Hyp | Ref
| Expression |
| 1 | | frlmphl.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
| 2 | 1 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝐼 ∈ 𝑊) |
| 3 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ 𝑉) |
| 4 | | frlmphl.y |
. . . . . . . . 9
⊢ 𝑌 = (𝑅 freeLMod 𝐼) |
| 5 | | frlmphl.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
| 6 | | frlmphl.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑌) |
| 7 | 4, 5, 6 | frlmbasmap 21779 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑m 𝐼)) |
| 8 | 2, 3, 7 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑m 𝐼)) |
| 9 | | elmapi 8889 |
. . . . . . 7
⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) → 𝑔:𝐼⟶𝐵) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔:𝐼⟶𝐵) |
| 11 | 10 | ffnd 6737 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 Fn 𝐼) |
| 12 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ 𝑉) |
| 13 | 4, 5, 6 | frlmbasmap 21779 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑m 𝐼)) |
| 14 | 2, 12, 13 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑m 𝐼)) |
| 15 | | elmapi 8889 |
. . . . . . 7
⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ:𝐼⟶𝐵) |
| 16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ:𝐼⟶𝐵) |
| 17 | 16 | ffnd 6737 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ Fn 𝐼) |
| 18 | | inidm 4227 |
. . . . 5
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
| 19 | | eqidd 2738 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
| 20 | | eqidd 2738 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥)) |
| 21 | 11, 17, 2, 2, 18, 19, 20 | offval 7706 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 ∘f · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) |
| 22 | 21 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑔 ∘f · ℎ) supp 0 ) = ((𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) supp 0 )) |
| 23 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 ∘f · ℎ) ∈ V) |
| 24 | | funmpt 6604 |
. . . . . 6
⊢ Fun
(𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) |
| 25 | | funeq 6586 |
. . . . . 6
⊢ ((𝑔 ∘f · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) → (Fun (𝑔 ∘f · ℎ) ↔ Fun (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) |
| 26 | 24, 25 | mpbiri 258 |
. . . . 5
⊢ ((𝑔 ∘f · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) → Fun (𝑔 ∘f · ℎ)) |
| 27 | 21, 26 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → Fun (𝑔 ∘f · ℎ)) |
| 28 | | frlmphl.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
| 29 | 4, 28, 6 | frlmbasfsupp 21778 |
. . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉) → 𝑔 finSupp 0 ) |
| 30 | 2, 3, 29 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 finSupp 0 ) |
| 31 | | frlmphl.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Field) |
| 32 | | isfld 20740 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
| 33 | 31, 32 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing)) |
| 34 | 33 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 35 | | drngring 20736 |
. . . . . . . 8
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
| 36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 37 | 36 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ Ring) |
| 38 | 5, 28 | ring0cl 20264 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
| 39 | 37, 38 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 0 ∈ 𝐵) |
| 40 | | frlmphl.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
| 41 | 5, 40, 28 | ringlz 20290 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵) → ( 0 · 𝑥) = 0 ) |
| 42 | 37, 41 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐵) → ( 0 · 𝑥) = 0 ) |
| 43 | 2, 39, 10, 16, 42 | suppofss1d 8229 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑔 ∘f · ℎ) supp 0 ) ⊆ (𝑔 supp 0 )) |
| 44 | | fsuppsssupp 9421 |
. . . . 5
⊢ ((((𝑔 ∘f · ℎ) ∈ V ∧ Fun (𝑔 ∘f · ℎ)) ∧ (𝑔 finSupp 0 ∧ ((𝑔 ∘f · ℎ) supp 0 ) ⊆ (𝑔 supp 0 ))) → (𝑔 ∘f · ℎ) finSupp 0 ) |
| 45 | 44 | fsuppimpd 9409 |
. . . 4
⊢ ((((𝑔 ∘f · ℎ) ∈ V ∧ Fun (𝑔 ∘f · ℎ)) ∧ (𝑔 finSupp 0 ∧ ((𝑔 ∘f · ℎ) supp 0 ) ⊆ (𝑔 supp 0 ))) → ((𝑔 ∘f · ℎ) supp 0 ) ∈
Fin) |
| 46 | 23, 27, 30, 43, 45 | syl22anc 839 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑔 ∘f · ℎ) supp 0 ) ∈
Fin) |
| 47 | 22, 46 | eqeltrrd 2842 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) supp 0 ) ∈
Fin) |
| 48 | 2 | mptexd 7244 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) ∈ V) |
| 49 | 39 | elexd 3504 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 0 ∈ V) |
| 50 | | funisfsupp 9407 |
. . 3
⊢ ((Fun
(𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) ∧ (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) supp 0 ) ∈
Fin)) |
| 51 | 24, 48, 49, 50 | mp3an2i 1468 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 ↔ ((𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) supp 0 ) ∈
Fin)) |
| 52 | 47, 51 | mpbird 257 |
1
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 ) |