lincresunit2

Description: Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019)

	Ref	Expression
Hypotheses	lincresunit.b	$⊢ B = {Base}_{M}$
	lincresunit.r	$⊢ R = Scalar (M)$
	lincresunit.e	$⊢ E = {Base}_{R}$
	lincresunit.u	$⊢ U = Unit (R)$
	lincresunit.0	$⊢ \underset{˙}{0} = 0_{R}$
	lincresunit.z	$⊢ Z = 0_{M}$
	lincresunit.n	$⊢ N = {inv}_{g} (R)$
	lincresunit.i	$⊢ I = {inv}_{r} (R)$
	lincresunit.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	lincresunit.g	$⊢ G = (s \in (S ∖ \{X\}) ⟼ I (N (F (X))) \underset{˙}{\cdot} F (s))$
Assertion	lincresunit2	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F))) \to {finSupp}_{\underset{˙}{0}} (G)$

Proof

Step	Hyp	Ref	Expression
1		lincresunit.b	$⊢ B = {Base}_{M}$
2		lincresunit.r	$⊢ R = Scalar (M)$
3		lincresunit.e	$⊢ E = {Base}_{R}$
4		lincresunit.u	$⊢ U = Unit (R)$
5		lincresunit.0	$⊢ \underset{˙}{0} = 0_{R}$
6		lincresunit.z	$⊢ Z = 0_{M}$
7		lincresunit.n	$⊢ N = {inv}_{g} (R)$
8		lincresunit.i	$⊢ I = {inv}_{r} (R)$
9		lincresunit.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
10		lincresunit.g	$⊢ G = (s \in (S ∖ \{X\}) ⟼ I (N (F (X))) \underset{˙}{\cdot} F (s))$
11		difexg	$⊢ S \in 𝒫 B \to S ∖ \{X\} \in V$
12	11	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S ∖ \{X\} \in V$
13	12	adantl	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to S ∖ \{X\} \in V$
14	13	adantr	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to S ∖ \{X\} \in V$
15		mptexg	$⊢ S ∖ \{X\} \in V \to (s \in (S ∖ \{X\}) ⟼ I (N (F (X))) \underset{˙}{\cdot} F (s)) \in V$
16	10 15	eqeltrid	$⊢ S ∖ \{X\} \in V \to G \in V$
17	14 16	syl	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to G \in V$
18	10	funmpt2	$⊢ Fun G$
19	18	a1i	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to Fun G$
20	5	fvexi	$⊢ \underset{˙}{0} \in V$
21	20	a1i	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to \underset{˙}{0} \in V$
22		simpr	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to {finSupp}_{\underset{˙}{0}} (F)$
23	22	fsuppimpd	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to F supp \underset{˙}{0} \in Fin$
24		simplr	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land s \in (S ∖ \{X\})) \to (S \in 𝒫 B \land M \in LMod \land X \in S)$
25		simpll	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land s \in (S ∖ \{X\})) \to (F \in (E^{S}) \land F (X) \in U)$
26		eldifi	$⊢ s \in (S ∖ \{X\}) \to s \in S$
27	26	adantl	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land s \in (S ∖ \{X\})) \to s \in S$
28	1 2 3 4 5 6 7 8 9 10	lincresunitlem2	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land s \in S) \to I (N (F (X))) \underset{˙}{\cdot} F (s) \in E$
29	24 25 27 28	syl21anc	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land s \in (S ∖ \{X\})) \to I (N (F (X))) \underset{˙}{\cdot} F (s) \in E$
30	29	ralrimiva	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to \forall s \in (S ∖ \{X\}) I (N (F (X))) \underset{˙}{\cdot} F (s) \in E$
31	10	fnmpt	$⊢ \forall s \in (S ∖ \{X\}) I (N (F (X))) \underset{˙}{\cdot} F (s) \in E \to G Fn (S ∖ \{X\})$
32	30 31	syl	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to G Fn (S ∖ \{X\})$
33		elmapfn	$⊢ F \in (E^{S}) \to F Fn S$
34	33	adantr	$⊢ (F \in (E^{S}) \land F (X) \in U) \to F Fn S$
35	34	adantr	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to F Fn S$
36	32 35	jca	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to (G Fn (S ∖ \{X\}) \land F Fn S)$
37		difssd	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to S ∖ \{X\} \subseteq S$
38		simpr1	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to S \in 𝒫 B$
39	20	a1i	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to \underset{˙}{0} \in V$
40	37 38 39	3jca	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to (S ∖ \{X\} \subseteq S \land S \in 𝒫 B \land \underset{˙}{0} \in V)$
41		fveq2	$⊢ s = x \to F (s) = F (x)$
42	41	oveq2d	$⊢ s = x \to I (N (F (X))) \underset{˙}{\cdot} F (s) = I (N (F (X))) \underset{˙}{\cdot} F (x)$
43		simplr	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to x \in (S ∖ \{X\})$
44		simpllr	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to (S \in 𝒫 B \land M \in LMod \land X \in S)$
45		simpll	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \to (F \in (E^{S}) \land F (X) \in U)$
46	45	adantr	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to (F \in (E^{S}) \land F (X) \in U)$
47		eldifi	$⊢ x \in (S ∖ \{X\}) \to x \in S$
48	47	adantl	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \to x \in S$
49	48	adantr	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to x \in S$
50	1 2 3 4 5 6 7 8 9 10	lincresunitlem2	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land x \in S) \to I (N (F (X))) \underset{˙}{\cdot} F (x) \in E$
51	44 46 49 50	syl21anc	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to I (N (F (X))) \underset{˙}{\cdot} F (x) \in E$
52	10 42 43 51	fvmptd3	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to G (x) = I (N (F (X))) \underset{˙}{\cdot} F (x)$
53		oveq2	$⊢ F (x) = \underset{˙}{0} \to I (N (F (X))) \underset{˙}{\cdot} F (x) = I (N (F (X))) \underset{˙}{\cdot} \underset{˙}{0}$
54	2	lmodring	$⊢ M \in LMod \to R \in Ring$
55	54	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to R \in Ring$
56	55	adantl	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to R \in Ring$
57	1 2 3 4 5 6 7 8 9 10	lincresunitlem1	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \to I (N (F (X))) \in E$
58	57	ancoms	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to I (N (F (X))) \in E$
59	3 9 5	ringrz	$⊢ (R \in Ring \land I (N (F (X))) \in E) \to I (N (F (X))) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
60	56 58 59	syl2anc	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to I (N (F (X))) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
61	60	adantr	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \to I (N (F (X))) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
62	53 61	sylan9eqr	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to I (N (F (X))) \underset{˙}{\cdot} F (x) = \underset{˙}{0}$
63	52 62	eqtrd	$⊢ ((((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \land F (x) = \underset{˙}{0}) \to G (x) = \underset{˙}{0}$
64	63	ex	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land x \in (S ∖ \{X\})) \to (F (x) = \underset{˙}{0} \to G (x) = \underset{˙}{0})$
65	64	ralrimiva	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to \forall x \in (S ∖ \{X\}) (F (x) = \underset{˙}{0} \to G (x) = \underset{˙}{0})$
66		suppfnss	$⊢ ((G Fn (S ∖ \{X\}) \land F Fn S) \land (S ∖ \{X\} \subseteq S \land S \in 𝒫 B \land \underset{˙}{0} \in V)) \to (\forall x \in (S ∖ \{X\}) (F (x) = \underset{˙}{0} \to G (x) = \underset{˙}{0}) \to G supp \underset{˙}{0} \subseteq F supp \underset{˙}{0})$
67	66	imp	$⊢ (((G Fn (S ∖ \{X\}) \land F Fn S) \land (S ∖ \{X\} \subseteq S \land S \in 𝒫 B \land \underset{˙}{0} \in V)) \land \forall x \in (S ∖ \{X\}) (F (x) = \underset{˙}{0} \to G (x) = \underset{˙}{0})) \to G supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
68	36 40 65 67	syl21anc	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to G supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
69	68	adantr	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to G supp \underset{˙}{0} \subseteq F supp \underset{˙}{0}$
70		suppssfifsupp	$⊢ ((G \in V \land Fun G \land \underset{˙}{0} \in V) \land (F supp \underset{˙}{0} \in Fin \land G supp \underset{˙}{0} \subseteq F supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} (G)$
71	17 19 21 23 69 70	syl32anc	$⊢ (((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \land {finSupp}_{\underset{˙}{0}} (F)) \to {finSupp}_{\underset{˙}{0}} (G)$
72	71	ex	$⊢ ((F \in (E^{S}) \land F (X) \in U) \land (S \in 𝒫 B \land M \in LMod \land X \in S)) \to ({finSupp}_{\underset{˙}{0}} (F) \to {finSupp}_{\underset{˙}{0}} (G))$
73	72	ex	$⊢ (F \in (E^{S}) \land F (X) \in U) \to ((S \in 𝒫 B \land M \in LMod \land X \in S) \to ({finSupp}_{\underset{˙}{0}} (F) \to {finSupp}_{\underset{˙}{0}} (G)))$
74	73	com23	$⊢ (F \in (E^{S}) \land F (X) \in U) \to ({finSupp}_{\underset{˙}{0}} (F) \to ((S \in 𝒫 B \land M \in LMod \land X \in S) \to {finSupp}_{\underset{˙}{0}} (G)))$
75	74	3impia	$⊢ (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F)) \to ((S \in 𝒫 B \land M \in LMod \land X \in S) \to {finSupp}_{\underset{˙}{0}} (G))$
76	75	impcom	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F))) \to {finSupp}_{\underset{˙}{0}} (G)$

Metamath Proof Explorer

Theorem lincresunit2

Proof