Step |
Hyp |
Ref |
Expression |
1 |
|
frlmphl.y |
⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 ) |
2 |
|
frlmphl.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
3 |
|
frlmphl.t |
⊢ · = ( .r ‘ 𝑅 ) |
4 |
|
frlmphl.v |
⊢ 𝑉 = ( Base ‘ 𝑌 ) |
5 |
|
frlmphl.j |
⊢ , = ( ·𝑖 ‘ 𝑌 ) |
6 |
|
frlmphl.o |
⊢ 𝑂 = ( 0g ‘ 𝑌 ) |
7 |
|
frlmphl.0 |
⊢ 0 = ( 0g ‘ 𝑅 ) |
8 |
|
frlmphl.s |
⊢ ∗ = ( *𝑟 ‘ 𝑅 ) |
9 |
|
frlmphl.f |
⊢ ( 𝜑 → 𝑅 ∈ Field ) |
10 |
|
frlmphl.m |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ( 𝑔 , 𝑔 ) = 0 ) → 𝑔 = 𝑂 ) |
11 |
|
frlmphl.u |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∗ ‘ 𝑥 ) = 𝑥 ) |
12 |
|
frlmphl.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
13 |
12
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝐼 ∈ 𝑊 ) |
14 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 ∈ 𝑉 ) |
15 |
1 2 4
|
frlmbasmap |
⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉 ) → 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ) |
16 |
13 14 15
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ) |
17 |
|
elmapi |
⊢ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ 𝐵 ) |
18 |
16 17
|
syl |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 : 𝐼 ⟶ 𝐵 ) |
19 |
18
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 Fn 𝐼 ) |
20 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ ∈ 𝑉 ) |
21 |
1 2 4
|
frlmbasmap |
⊢ ( ( 𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉 ) → ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) |
22 |
13 20 21
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) |
23 |
|
elmapi |
⊢ ( ℎ ∈ ( 𝐵 ↑m 𝐼 ) → ℎ : 𝐼 ⟶ 𝐵 ) |
24 |
22 23
|
syl |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ : 𝐼 ⟶ 𝐵 ) |
25 |
24
|
ffnd |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ Fn 𝐼 ) |
26 |
|
inidm |
⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼 |
27 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) |
28 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) |
29 |
19 25 13 13 26 27 28
|
offval |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑔 ∘f · ℎ ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) |
30 |
29
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ( 𝑔 ∘f · ℎ ) supp 0 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) supp 0 ) ) |
31 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑔 ∘f · ℎ ) ∈ V ) |
32 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) |
33 |
|
funeq |
⊢ ( ( 𝑔 ∘f · ℎ ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) → ( Fun ( 𝑔 ∘f · ℎ ) ↔ Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) ) |
34 |
32 33
|
mpbiri |
⊢ ( ( 𝑔 ∘f · ℎ ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) → Fun ( 𝑔 ∘f · ℎ ) ) |
35 |
29 34
|
syl |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → Fun ( 𝑔 ∘f · ℎ ) ) |
36 |
1 7 4
|
frlmbasfsupp |
⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉 ) → 𝑔 finSupp 0 ) |
37 |
13 14 36
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 finSupp 0 ) |
38 |
|
isfld |
⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) ) |
39 |
9 38
|
sylib |
⊢ ( 𝜑 → ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) ) |
40 |
39
|
simpld |
⊢ ( 𝜑 → 𝑅 ∈ DivRing ) |
41 |
|
drngring |
⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring ) |
42 |
40 41
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
43 |
42
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑅 ∈ Ring ) |
44 |
2 7
|
ring0cl |
⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 ) |
45 |
43 44
|
syl |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 0 ∈ 𝐵 ) |
46 |
2 3 7
|
ringlz |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 0 · 𝑥 ) = 0 ) |
47 |
43 46
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 · 𝑥 ) = 0 ) |
48 |
13 45 18 24 47
|
suppofss1d |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ( 𝑔 ∘f · ℎ ) supp 0 ) ⊆ ( 𝑔 supp 0 ) ) |
49 |
|
fsuppsssupp |
⊢ ( ( ( ( 𝑔 ∘f · ℎ ) ∈ V ∧ Fun ( 𝑔 ∘f · ℎ ) ) ∧ ( 𝑔 finSupp 0 ∧ ( ( 𝑔 ∘f · ℎ ) supp 0 ) ⊆ ( 𝑔 supp 0 ) ) ) → ( 𝑔 ∘f · ℎ ) finSupp 0 ) |
50 |
49
|
fsuppimpd |
⊢ ( ( ( ( 𝑔 ∘f · ℎ ) ∈ V ∧ Fun ( 𝑔 ∘f · ℎ ) ) ∧ ( 𝑔 finSupp 0 ∧ ( ( 𝑔 ∘f · ℎ ) supp 0 ) ⊆ ( 𝑔 supp 0 ) ) ) → ( ( 𝑔 ∘f · ℎ ) supp 0 ) ∈ Fin ) |
51 |
31 35 37 48 50
|
syl22anc |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ( 𝑔 ∘f · ℎ ) supp 0 ) ∈ Fin ) |
52 |
30 51
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) supp 0 ) ∈ Fin ) |
53 |
13
|
mptexd |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ∈ V ) |
54 |
45
|
elexd |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 0 ∈ V ) |
55 |
|
funisfsupp |
⊢ ( ( Fun ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) supp 0 ) ∈ Fin ) ) |
56 |
32 53 54 55
|
mp3an2i |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) supp 0 ) ∈ Fin ) ) |
57 |
52 56
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) finSupp 0 ) |