frlmphllem

	Ref	Expression
Hypotheses	frlmphl.y	$⊢ Y = R freeLMod I$
	frlmphl.b	$⊢ B = {Base}_{R}$
	frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	frlmphl.v	$⊢ V = {Base}_{Y}$
	frlmphl.j	$⊢ \underset{˙}{,} = \cdot_{𝑖} (Y)$
	frlmphl.o	$⊢ O = 0_{Y}$
	frlmphl.0	$⊢ \underset{˙}{0} = 0_{R}$
	frlmphl.s	$⊢ \underset{˙}{} = _{R}$
	frlmphl.f	$⊢ φ \to R \in Field$
	frlmphl.m	$⊢ (φ \land g \in V \land g \underset{˙}{,} g = \underset{˙}{0}) \to g = O$
	frlmphl.u	$⊢ (φ \land x \in B) \to \underset{˙}{*} (x) = x$
	frlmphl.i	$⊢ φ \to I \in W$
Assertion	frlmphllem	$⊢ (φ \land g \in V \land h \in V) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)))$

Proof

Step	Hyp	Ref	Expression
1		frlmphl.y	$⊢ Y = R freeLMod I$
2		frlmphl.b	$⊢ B = {Base}_{R}$
3		frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		frlmphl.v	$⊢ V = {Base}_{Y}$
5		frlmphl.j	$⊢ \underset{˙}{,} = \cdot_{𝑖} (Y)$
6		frlmphl.o	$⊢ O = 0_{Y}$
7		frlmphl.0	$⊢ \underset{˙}{0} = 0_{R}$
8		frlmphl.s	$⊢ \underset{˙}{} = _{R}$
9		frlmphl.f	$⊢ φ \to R \in Field$
10		frlmphl.m	$⊢ (φ \land g \in V \land g \underset{˙}{,} g = \underset{˙}{0}) \to g = O$
11		frlmphl.u	$⊢ (φ \land x \in B) \to \underset{˙}{*} (x) = x$
12		frlmphl.i	$⊢ φ \to I \in W$
13	12	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to I \in W$
14		simp2	$⊢ (φ \land g \in V \land h \in V) \to g \in V$
15	1 2 4	frlmbasmap	$⊢ (I \in W \land g \in V) \to g \in (B^{I})$
16	13 14 15	syl2anc	$⊢ (φ \land g \in V \land h \in V) \to g \in (B^{I})$
17		elmapi	$⊢ g \in (B^{I}) \to g : I ⟶ B$
18	16 17	syl	$⊢ (φ \land g \in V \land h \in V) \to g : I ⟶ B$
19	18	ffnd	$⊢ (φ \land g \in V \land h \in V) \to g Fn I$
20		simp3	$⊢ (φ \land g \in V \land h \in V) \to h \in V$
21	1 2 4	frlmbasmap	$⊢ (I \in W \land h \in V) \to h \in (B^{I})$
22	13 20 21	syl2anc	$⊢ (φ \land g \in V \land h \in V) \to h \in (B^{I})$
23		elmapi	$⊢ h \in (B^{I}) \to h : I ⟶ B$
24	22 23	syl	$⊢ (φ \land g \in V \land h \in V) \to h : I ⟶ B$
25	24	ffnd	$⊢ (φ \land g \in V \land h \in V) \to h Fn I$
26		inidm	$⊢ I \cap I = I$
27		eqidd	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to g (x) = g (x)$
28		eqidd	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to h (x) = h (x)$
29	19 25 13 13 26 27 28	offval	$⊢ (φ \land g \in V \land h \in V) \to g {\underset{˙}{\cdot}}_{f} h = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))$
30	29	oveq1d	$⊢ (φ \land g \in V \land h \in V) \to (g {\underset{˙}{\cdot}}_{f} h) supp \underset{˙}{0} = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) supp \underset{˙}{0}$
31		ovexd	$⊢ (φ \land g \in V \land h \in V) \to g {\underset{˙}{\cdot}}_{f} h \in V$
32		funmpt	$⊢ Fun (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))$
33		funeq	$⊢ g {\underset{˙}{\cdot}}_{f} h = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) \to (Fun (g {\underset{˙}{\cdot}}_{f} h) \leftrightarrow Fun (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)))$
34	32 33	mpbiri	$⊢ g {\underset{˙}{\cdot}}_{f} h = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) \to Fun (g {\underset{˙}{\cdot}}_{f} h)$
35	29 34	syl	$⊢ (φ \land g \in V \land h \in V) \to Fun (g {\underset{˙}{\cdot}}_{f} h)$
36	1 7 4	frlmbasfsupp	$⊢ (I \in W \land g \in V) \to {finSupp}_{\underset{˙}{0}} (g)$
37	13 14 36	syl2anc	$⊢ (φ \land g \in V \land h \in V) \to {finSupp}_{\underset{˙}{0}} (g)$
38		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
39	9 38	sylib	$⊢ φ \to (R \in DivRing \land R \in CRing)$
40	39	simpld	$⊢ φ \to R \in DivRing$
41		drngring	$⊢ R \in DivRing \to R \in Ring$
42	40 41	syl	$⊢ φ \to R \in Ring$
43	42	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to R \in Ring$
44	2 7	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
45	43 44	syl	$⊢ (φ \land g \in V \land h \in V) \to \underset{˙}{0} \in B$
46	2 3 7	ringlz	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
47	43 46	sylan	$⊢ ((φ \land g \in V \land h \in V) \land x \in B) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
48	13 45 18 24 47	suppofss1d	$⊢ (φ \land g \in V \land h \in V) \to (g {\underset{˙}{\cdot}}_{f} h) supp \underset{˙}{0} \subseteq g supp \underset{˙}{0}$
49		fsuppsssupp	$⊢ ((g {\underset{˙}{\cdot}}_{f} h \in V \land Fun (g {\underset{˙}{\cdot}}_{f} h)) \land ({finSupp}_{\underset{˙}{0}} (g) \land (g {\underset{˙}{\cdot}}_{f} h) supp \underset{˙}{0} \subseteq g supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((g {\underset{˙}{\cdot}}_{f} h))$
50	49	fsuppimpd	$⊢ ((g {\underset{˙}{\cdot}}_{f} h \in V \land Fun (g {\underset{˙}{\cdot}}_{f} h)) \land ({finSupp}_{\underset{˙}{0}} (g) \land (g {\underset{˙}{\cdot}}_{f} h) supp \underset{˙}{0} \subseteq g supp \underset{˙}{0})) \to (g {\underset{˙}{\cdot}}_{f} h) supp \underset{˙}{0} \in Fin$
51	31 35 37 48 50	syl22anc	$⊢ (φ \land g \in V \land h \in V) \to (g {\underset{˙}{\cdot}}_{f} h) supp \underset{˙}{0} \in Fin$
52	30 51	eqeltrrd	$⊢ (φ \land g \in V \land h \in V) \to (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) supp \underset{˙}{0} \in Fin$
53	13	mptexd	$⊢ (φ \land g \in V \land h \in V) \to (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) \in V$
54	45	elexd	$⊢ (φ \land g \in V \land h \in V) \to \underset{˙}{0} \in V$
55		funisfsupp	$⊢ (Fun (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) \land (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))) \leftrightarrow (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) supp \underset{˙}{0} \in Fin)$
56	32 53 54 55	mp3an2i	$⊢ (φ \land g \in V \land h \in V) \to ({finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))) \leftrightarrow (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) supp \underset{˙}{0} \in Fin)$
57	52 56	mpbird	$⊢ (φ \land g \in V \land h \in V) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)))$

Metamath Proof Explorer

Theorem frlmphllem

Proof