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 )