lincresunit3

Description: Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019) (Proof shortened by AV, 30-Jul-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	lincresunit3	$⊢ ((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)) \land F linC (M) S = Z) \to G linC (M) (S ∖ \{X\}) = X$

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		simp2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to M \in LMod$
12	11	3ad2ant1	$⊢ ((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)) \land F linC (M) S = Z) \to M \in LMod$
13		simp1	$⊢ ((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)) \land F linC (M) S = Z) \to (S \in 𝒫 B \land M \in LMod \land X \in S)$
14		3simpa	$⊢ (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F)) \to (F \in (E^{S}) \land F (X) \in U)$
15	14	3ad2ant2	$⊢ ((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)) \land F linC (M) S = Z) \to (F \in (E^{S}) \land F (X) \in U)$
16	13 15	jca	$⊢ ((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)) \land F linC (M) S = Z) \to ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U))$
17		eldifi	$⊢ s \in (S ∖ \{X\}) \to s \in S$
18	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$
19	16 17 18	syl2an	$⊢ (((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)) \land F linC (M) S = Z) \land s \in (S ∖ \{X\})) \to I (N (F (X))) \underset{˙}{\cdot} F (s) \in E$
20	2	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
21	3 20	eqtri	$⊢ E = {Base}_{Scalar (M)}$
22	19 21	eleqtrdi	$⊢ (((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)) \land F linC (M) S = Z) \land s \in (S ∖ \{X\})) \to I (N (F (X))) \underset{˙}{\cdot} F (s) \in {Base}_{Scalar (M)}$
23	22 10	fmptd	$⊢ ((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)) \land F linC (M) S = Z) \to G : S ∖ \{X\} ⟶ {Base}_{Scalar (M)}$
24		fvex	$⊢ {Base}_{Scalar (M)} \in V$
25		difexg	$⊢ S \in 𝒫 B \to S ∖ \{X\} \in V$
26	25	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S ∖ \{X\} \in V$
27	26	3ad2ant1	$⊢ ((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)) \land F linC (M) S = Z) \to S ∖ \{X\} \in V$
28		elmapg	$⊢ ({Base}_{Scalar (M)} \in V \land S ∖ \{X\} \in V) \to (G \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})}) \leftrightarrow G : S ∖ \{X\} ⟶ {Base}_{Scalar (M)})$
29	24 27 28	sylancr	$⊢ ((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)) \land F linC (M) S = Z) \to (G \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})}) \leftrightarrow G : S ∖ \{X\} ⟶ {Base}_{Scalar (M)})$
30	23 29	mpbird	$⊢ ((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)) \land F linC (M) S = Z) \to G \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})})$
31		difexg	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{X\} \in V$
32	31	adantl	$⊢ (X \in S \land S \in 𝒫 {Base}_{M}) \to S ∖ \{X\} \in V$
33		ssdifss	$⊢ S \subseteq {Base}_{M} \to S ∖ \{X\} \subseteq {Base}_{M}$
34	33	a1i	$⊢ X \in S \to (S \subseteq {Base}_{M} \to S ∖ \{X\} \subseteq {Base}_{M})$
35		elpwi	$⊢ S \in 𝒫 {Base}_{M} \to S \subseteq {Base}_{M}$
36	34 35	impel	$⊢ (X \in S \land S \in 𝒫 {Base}_{M}) \to S ∖ \{X\} \subseteq {Base}_{M}$
37	32 36	elpwd	$⊢ (X \in S \land S \in 𝒫 {Base}_{M}) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
38	37	expcom	$⊢ S \in 𝒫 {Base}_{M} \to (X \in S \to S ∖ \{X\} \in 𝒫 {Base}_{M})$
39	1	pweqi	$⊢ 𝒫 B = 𝒫 {Base}_{M}$
40	38 39	eleq2s	$⊢ S \in 𝒫 B \to (X \in S \to S ∖ \{X\} \in 𝒫 {Base}_{M})$
41	40	imp	$⊢ (S \in 𝒫 B \land X \in S) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
42	41	3adant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
43	42	3ad2ant1	$⊢ ((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)) \land F linC (M) S = Z) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
44		lincval	$⊢ (M \in LMod \land G \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})}) \land S ∖ \{X\} \in 𝒫 {Base}_{M}) \to G linC (M) (S ∖ \{X\}) = \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s)$
45	12 30 43 44	syl3anc	$⊢ ((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)) \land F linC (M) S = Z) \to G linC (M) (S ∖ \{X\}) = \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s)$
46		simp1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S \in 𝒫 B$
47		simp3	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to X \in S$
48	11 46 47	3jca	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to (M \in LMod \land S \in 𝒫 B \land X \in S)$
49	48	adantr	$⊢ ((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 (M \in LMod \land S \in 𝒫 B \land X \in S)$
50		3simpb	$⊢ (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F)) \to (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F))$
51	50	adantl	$⊢ ((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 (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F))$
52		eqidd	$⊢ ((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 {F ↾}_{(S ∖ \{X\})} = {F ↾}_{(S ∖ \{X\})}$
53		eqid	$⊢ \cdot_{M} = \cdot_{M}$
54		eqid	$⊢ +_{M} = +_{M}$
55	1 2 3 53 54 5	lincdifsn	$⊢ ((M \in LMod \land S \in 𝒫 B \land X \in S) \land (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F)) \land {F ↾}_{(S ∖ \{X\})} = {F ↾}_{(S ∖ \{X\})}) \to F linC (M) S = (({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X)$
56	49 51 52 55	syl3anc	$⊢ ((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 F linC (M) S = (({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X)$
57	56	eqeq1d	$⊢ ((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 (F linC (M) S = Z \leftrightarrow (({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = Z)$
58		fveq2	$⊢ s = z \to G (s) = G (z)$
59		id	$⊢ s = z \to s = z$
60	58 59	oveq12d	$⊢ s = z \to G (s) \cdot_{M} s = G (z) \cdot_{M} z$
61	60	cbvmptv	$⊢ (s \in (S ∖ \{X\}) ⟼ G (s) \cdot_{M} s) = (z \in (S ∖ \{X\}) ⟼ G (z) \cdot_{M} z)$
62	61	a1i	$⊢ ((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 (s \in (S ∖ \{X\}) ⟼ G (s) \cdot_{M} s) = (z \in (S ∖ \{X\}) ⟼ G (z) \cdot_{M} z)$
63	62	oveq2d	$⊢ ((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 \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = \underset{z \in S ∖ \{X\}}{\sum_{M}} (G (z) \cdot_{M} z)$
64	63	oveq2d	$⊢ ((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 N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) = N (F (X)) \cdot_{M} (\underset{z \in S ∖ \{X\}}{\sum_{M}}, (G (z) \cdot_{M} z))$
65	1 2 3 4 5 6 7 8 9 10	lincresunit3lem2	$⊢ ((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 N (F (X)) \cdot_{M} (\underset{z \in S ∖ \{X\}}{\sum_{M}}, (G (z) \cdot_{M} z)) = ({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})$
66	64 65	eqtr2d	$⊢ ((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 ({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\}) = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s))$
67	66	oveq1d	$⊢ ((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 (({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = (N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s))) +_{M} (F (X) \cdot_{M} X)$
68	67	eqeq1d	$⊢ ((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 ((({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = Z \leftrightarrow (N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s))) +_{M} (F (X) \cdot_{M} X) = Z)$
69		lmodgrp	$⊢ M \in LMod \to M \in Grp$
70	69	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to M \in Grp$
71	70	adantr	$⊢ ((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 M \in Grp$
72	11	adantr	$⊢ ((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 M \in LMod$
73		elmapi	$⊢ F \in (E^{S}) \to F : S ⟶ E$
74	73	3ad2ant1	$⊢ (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F)) \to F : S ⟶ E$
75		ffvelrn	$⊢ (F : S ⟶ E \land X \in S) \to F (X) \in E$
76	74 47 75	syl2anr	$⊢ ((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 F (X) \in E$
77		elpwi	$⊢ S \in 𝒫 B \to S \subseteq B$
78	77	sselda	$⊢ (S \in 𝒫 B \land X \in S) \to X \in B$
79	78	3adant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to X \in B$
80	79	adantr	$⊢ ((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 X \in B$
81	1 2 53 3	lmodvscl	$⊢ (M \in LMod \land F (X) \in E \land X \in B) \to F (X) \cdot_{M} X \in B$
82	72 76 80 81	syl3anc	$⊢ ((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 F (X) \cdot_{M} X \in B$
83	2	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
84	83	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to R \in Grp$
85	3 7	grpinvcl	$⊢ (R \in Grp \land F (X) \in E) \to N (F (X)) \in E$
86	84 76 85	syl2an2r	$⊢ ((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 N (F (X)) \in E$
87		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
88	87	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to M \in CMnd$
89	88	adantr	$⊢ ((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 M \in CMnd$
90	26	adantr	$⊢ ((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 S ∖ \{X\} \in V$
91		simpll2	$⊢ (((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))) \land s \in (S ∖ \{X\})) \to M \in LMod$
92	1 2 3 4 5 6 7 8 9 10	lincresunit1	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \to G \in (E^{(S ∖ \{X\})})$
93	92	3adantr3	$⊢ ((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 G \in (E^{(S ∖ \{X\})})$
94		elmapi	$⊢ G \in (E^{(S ∖ \{X\})}) \to G : S ∖ \{X\} ⟶ E$
95	93 94	syl	$⊢ ((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 G : S ∖ \{X\} ⟶ E$
96	95	ffvelrnda	$⊢ (((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))) \land s \in (S ∖ \{X\})) \to G (s) \in E$
97		ssel2	$⊢ (S \subseteq B \land s \in S) \to s \in B$
98	97	expcom	$⊢ s \in S \to (S \subseteq B \to s \in B)$
99	17 77 98	syl2imc	$⊢ S \in 𝒫 B \to (s \in (S ∖ \{X\}) \to s \in B)$
100	99	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to (s \in (S ∖ \{X\}) \to s \in B)$
101	100	adantr	$⊢ ((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 (s \in (S ∖ \{X\}) \to s \in B)$
102	101	imp	$⊢ (((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))) \land s \in (S ∖ \{X\})) \to s \in B$
103	1 2 53 3	lmodvscl	$⊢ (M \in LMod \land G (s) \in E \land s \in B) \to G (s) \cdot_{M} s \in B$
104	91 96 102 103	syl3anc	$⊢ (((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))) \land s \in (S ∖ \{X\})) \to G (s) \cdot_{M} s \in B$
105	104	fmpttd	$⊢ ((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 (s \in (S ∖ \{X\}) ⟼ G (s) \cdot_{M} s) : S ∖ \{X\} ⟶ B$
106	25	adantr	$⊢ (S \in 𝒫 B \land X \in S) \to S ∖ \{X\} \in V$
107		ssdifss	$⊢ S \subseteq B \to S ∖ \{X\} \subseteq B$
108	77 107	syl	$⊢ S \in 𝒫 B \to S ∖ \{X\} \subseteq B$
109	108	adantr	$⊢ (S \in 𝒫 B \land X \in S) \to S ∖ \{X\} \subseteq B$
110	109 1	sseqtrdi	$⊢ (S \in 𝒫 B \land X \in S) \to S ∖ \{X\} \subseteq {Base}_{M}$
111	106 110	elpwd	$⊢ (S \in 𝒫 B \land X \in S) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
112	111	3adant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
113	11 112	jca	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to (M \in LMod \land S ∖ \{X\} \in 𝒫 {Base}_{M})$
114	113	adantr	$⊢ ((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 (M \in LMod \land S ∖ \{X\} \in 𝒫 {Base}_{M})$
115	1 2 3 4 5 6 7 8 9 10	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)$
116	115 5	breqtrdi	$⊢ ((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}_{0_{R}} (G)$
117	2 3	scmfsupp	$⊢ ((M \in LMod \land S ∖ \{X\} \in 𝒫 {Base}_{M}) \land G \in (E^{(S ∖ \{X\})}) \land {finSupp}_{0_{R}} (G)) \to {finSupp}_{0_{M}} ((s \in (S ∖ \{X\}) ⟼ G (s) \cdot_{M} s))$
118	114 93 116 117	syl3anc	$⊢ ((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}_{0_{M}} ((s \in (S ∖ \{X\}) ⟼ G (s) \cdot_{M} s))$
119	118 6	breqtrrdi	$⊢ ((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}_{Z} ((s \in (S ∖ \{X\}) ⟼ G (s) \cdot_{M} s))$
120	1 6 89 90 105 119	gsumcl	$⊢ ((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 \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) \in B$
121	1 2 53 3	lmodvscl	$⊢ (M \in LMod \land N (F (X)) \in E \land \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) \in B) \to N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \in B$
122	72 86 120 121	syl3anc	$⊢ ((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 N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \in B$
123		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
124	1 54 6 123	grpinvid2	$⊢ (M \in Grp \land F (X) \cdot_{M} X \in B \land N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \in B) \to ({inv}_{g} (M) (F (X) \cdot_{M} X) = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \leftrightarrow (N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s))) +_{M} (F (X) \cdot_{M} X) = Z)$
125	71 82 122 124	syl3anc	$⊢ ((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 ({inv}_{g} (M) (F (X) \cdot_{M} X) = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \leftrightarrow (N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s))) +_{M} (F (X) \cdot_{M} X) = Z)$
126	1 2 53 123 3 7 72 80 76	lmodvsneg	$⊢ ((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 {inv}_{g} (M) (F (X) \cdot_{M} X) = N (F (X)) \cdot_{M} X$
127	126	eqeq1d	$⊢ ((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 ({inv}_{g} (M) (F (X) \cdot_{M} X) = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \leftrightarrow N (F (X)) \cdot_{M} X = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)))$
128		simpr2	$⊢ ((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 F (X) \in U$
129	1 2 3 4 7 53	lincresunit3lem3	$⊢ ((M \in LMod \land X \in B \land \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) \in B) \land F (X) \in U) \to (N (F (X)) \cdot_{M} X = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \leftrightarrow X = \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s))$
130		eqcom	$⊢ X = \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) \leftrightarrow \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X$
131	129 130	bitrdi	$⊢ ((M \in LMod \land X \in B \land \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) \in B) \land F (X) \in U) \to (N (F (X)) \cdot_{M} X = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \leftrightarrow \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
132	72 80 120 128 131	syl31anc	$⊢ ((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 (N (F (X)) \cdot_{M} X = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \leftrightarrow \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
133	132	biimpd	$⊢ ((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 (N (F (X)) \cdot_{M} X = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \to \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
134	127 133	sylbid	$⊢ ((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 ({inv}_{g} (M) (F (X) \cdot_{M} X) = N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s)) \to \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
135	125 134	sylbird	$⊢ ((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 ((N (F (X)) \cdot_{M} (\underset{s \in S ∖ \{X\}}{\sum_{M}}, (G (s) \cdot_{M} s))) +_{M} (F (X) \cdot_{M} X) = Z \to \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
136	68 135	sylbid	$⊢ ((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 ((({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = Z \to \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
137	57 136	sylbid	$⊢ ((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 (F linC (M) S = Z \to \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X)$
138	137	3impia	$⊢ ((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)) \land F linC (M) S = Z) \to \underset{s \in S ∖ \{X\}}{\sum_{M}} (G (s) \cdot_{M} s) = X$
139	45 138	eqtrd	$⊢ ((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)) \land F linC (M) S = Z) \to G linC (M) (S ∖ \{X\}) = X$

Metamath Proof Explorer

Theorem lincresunit3

Proof