Metamath Proof Explorer

Theorem frlmphllem

Description: Lemma for frlmphl . (Contributed by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmphl.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmphl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
frlmphl.t ⊢ · = ( .r ‘ 𝑅 )
frlmphl.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
frlmphl.j ⊢ , = ( ·𝑖 ‘ 𝑌 )
frlmphl.o ⊢ 𝑂 = ( 0g ‘ 𝑌 )
frlmphl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
frlmphl.s ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
frlmphl.f ⊢ ( 𝜑 → 𝑅 ∈ Field )
frlmphl.m ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ( 𝑔 , 𝑔 ) = 0 ) → 𝑔 = 𝑂 )
frlmphl.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∗ ‘ 𝑥 ) = 𝑥 )
frlmphl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
Assertion frlmphllem ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) finSupp 0 )

Proof

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 )