lincresunit3lem2

Description: Lemma 2 for lincresunit3 . (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	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\})$

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		simpl2	$⊢ ((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$
12	2	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
13	3 12	eqtri	$⊢ E = {Base}_{Scalar (M)}$
14	13	oveq1i	$⊢ E^{S} = {Base}_{Scalar (M)}^{S}$
15	14	eleq2i	$⊢ F \in (E^{S}) \leftrightarrow F \in ({Base}_{Scalar (M)}^{S})$
16	15	biimpi	$⊢ F \in (E^{S}) \to F \in ({Base}_{Scalar (M)}^{S})$
17	16	3ad2ant1	$⊢ (F \in (E^{S}) \land F (X) \in U \land {finSupp}_{\underset{˙}{0}} (F)) \to F \in ({Base}_{Scalar (M)}^{S})$
18	17	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 ({Base}_{Scalar (M)}^{S})$
19		difssd	$⊢ ((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\} \subseteq S$
20		elmapssres	$⊢ (F \in ({Base}_{Scalar (M)}^{S}) \land S ∖ \{X\} \subseteq S) \to {F ↾}_{(S ∖ \{X\})} \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})})$
21	18 19 20	syl2anc	$⊢ ((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\})} \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})})$
22		elpwi	$⊢ S \in 𝒫 {Base}_{M} \to S \subseteq {Base}_{M}$
23	22	ssdifssd	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{X\} \subseteq {Base}_{M}$
24		difexg	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{X\} \in V$
25		elpwg	$⊢ S ∖ \{X\} \in V \to (S ∖ \{X\} \in 𝒫 {Base}_{M} \leftrightarrow S ∖ \{X\} \subseteq {Base}_{M})$
26	24 25	syl	$⊢ S \in 𝒫 {Base}_{M} \to (S ∖ \{X\} \in 𝒫 {Base}_{M} \leftrightarrow S ∖ \{X\} \subseteq {Base}_{M})$
27	23 26	mpbird	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
28	1	pweqi	$⊢ 𝒫 B = 𝒫 {Base}_{M}$
29	27 28	eleq2s	$⊢ S \in 𝒫 B \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
30	29	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S ∖ \{X\} \in 𝒫 {Base}_{M}$
31	30	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 𝒫 {Base}_{M}$
32		lincval	$⊢ (M \in LMod \land {F ↾}_{(S ∖ \{X\})} \in ({Base}_{Scalar (M)}^{(S ∖ \{X\})}) \land S ∖ \{X\} \in 𝒫 {Base}_{M}) \to ({F ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\}) = \underset{z \in S ∖ \{X\}}{\sum_{M}} (({F ↾}_{(S ∖ \{X\})}) (z) \cdot_{M} z)$
33	11 21 31 32	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 ↾}_{(S ∖ \{X\})}) linC (M) (S ∖ \{X\}) = \underset{z \in S ∖ \{X\}}{\sum_{M}} (({F ↾}_{(S ∖ \{X\})}) (z) \cdot_{M} z)$
34		simpll	$⊢ (((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 z \in (S ∖ \{X\})) \to (S \in 𝒫 B \land M \in LMod \land X \in S)$
35		simplr1	$⊢ (((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 z \in (S ∖ \{X\})) \to F \in (E^{S})$
36		simplr2	$⊢ (((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 z \in (S ∖ \{X\})) \to F (X) \in U$
37		simpr	$⊢ (((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 z \in (S ∖ \{X\})) \to z \in (S ∖ \{X\})$
38	1 2 3 4 5 6 7 8 9 10	lincresunit3lem1	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \cdot_{M} (G (z) \cdot_{M} z) = F (z) \cdot_{M} z$
39	34 35 36 37 38	syl13anc	$⊢ (((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 z \in (S ∖ \{X\})) \to N (F (X)) \cdot_{M} (G (z) \cdot_{M} z) = F (z) \cdot_{M} z$
40		fvres	$⊢ z \in (S ∖ \{X\}) \to ({F ↾}_{(S ∖ \{X\})}) (z) = F (z)$
41	40	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))) \land z \in (S ∖ \{X\})) \to ({F ↾}_{(S ∖ \{X\})}) (z) = F (z)$
42	41	eqcomd	$⊢ (((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 z \in (S ∖ \{X\})) \to F (z) = ({F ↾}_{(S ∖ \{X\})}) (z)$
43	42	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))) \land z \in (S ∖ \{X\})) \to F (z) \cdot_{M} z = ({F ↾}_{(S ∖ \{X\})}) (z) \cdot_{M} z$
44	39 43	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 z \in (S ∖ \{X\})) \to N (F (X)) \cdot_{M} (G (z) \cdot_{M} z) = ({F ↾}_{(S ∖ \{X\})}) (z) \cdot_{M} z$
45	44	mpteq2dva	$⊢ ((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 (z \in (S ∖ \{X\}) ⟼ N (F (X)) \cdot_{M} (G (z) \cdot_{M} z)) = (z \in (S ∖ \{X\}) ⟼ ({F ↾}_{(S ∖ \{X\})}) (z) \cdot_{M} z)$
46	45	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{z \in S ∖ \{X\}}{\sum_{M}} (N (F (X)) \cdot_{M} (G (z) \cdot_{M} z)) = \underset{z \in S ∖ \{X\}}{\sum_{M}} (({F ↾}_{(S ∖ \{X\})}) (z) \cdot_{M} z)$
47		eqid	$⊢ +_{M} = +_{M}$
48		eqid	$⊢ \cdot_{M} = \cdot_{M}$
49		difexg	$⊢ S \in 𝒫 B \to S ∖ \{X\} \in V$
50	49	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to S ∖ \{X\} \in V$
51	50	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$
52	2	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
53	52	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to R \in Grp$
54	53	adantr	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land F \in (E^{S})) \to R \in Grp$
55		elmapi	$⊢ F \in (E^{S}) \to F : S ⟶ E$
56		ffvelrn	$⊢ (F : S ⟶ E \land X \in S) \to F (X) \in E$
57	56	expcom	$⊢ X \in S \to (F : S ⟶ E \to F (X) \in E)$
58	57	3ad2ant3	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to (F : S ⟶ E \to F (X) \in E)$
59	55 58	syl5com	$⊢ F \in (E^{S}) \to ((S \in 𝒫 B \land M \in LMod \land X \in S) \to F (X) \in E)$
60	59	impcom	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land F \in (E^{S})) \to F (X) \in E$
61	3 7	grpinvcl	$⊢ (R \in Grp \land F (X) \in E) \to N (F (X)) \in E$
62	54 60 61	syl2anc	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land F \in (E^{S})) \to N (F (X)) \in E$
63	62	3ad2antr1	$⊢ ((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$
64	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))) \land z \in (S ∖ \{X\})) \to M \in LMod$
65	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\})})$
66	65	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\})})$
67		elmapi	$⊢ G \in (E^{(S ∖ \{X\})}) \to G : S ∖ \{X\} ⟶ E$
68		ffvelrn	$⊢ (G : S ∖ \{X\} ⟶ E \land z \in (S ∖ \{X\})) \to G (z) \in E$
69	68	ex	$⊢ G : S ∖ \{X\} ⟶ E \to (z \in (S ∖ \{X\}) \to G (z) \in E)$
70	66 67 69	3syl	$⊢ ((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 (z \in (S ∖ \{X\}) \to G (z) \in E)$
71	70	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 z \in (S ∖ \{X\})) \to G (z) \in E$
72		elpwi	$⊢ S \in 𝒫 B \to S \subseteq B$
73		eldifi	$⊢ z \in (S ∖ \{X\}) \to z \in S$
74		ssel2	$⊢ (S \subseteq B \land z \in S) \to z \in B$
75	74	expcom	$⊢ z \in S \to (S \subseteq B \to z \in B)$
76	73 75	syl	$⊢ z \in (S ∖ \{X\}) \to (S \subseteq B \to z \in B)$
77	72 76	syl5com	$⊢ S \in 𝒫 B \to (z \in (S ∖ \{X\}) \to z \in B)$
78	77	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to (z \in (S ∖ \{X\}) \to z \in B)$
79	78	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 (z \in (S ∖ \{X\}) \to z \in B)$
80	79	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 z \in (S ∖ \{X\})) \to z \in B$
81	1 2 48 3	lmodvscl	$⊢ (M \in LMod \land G (z) \in E \land z \in B) \to G (z) \cdot_{M} z \in B$
82	64 71 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))) \land z \in (S ∖ \{X\})) \to G (z) \cdot_{M} z \in B$
83		simp2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to M \in LMod$
84	83 30	jca	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to (M \in LMod \land S ∖ \{X\} \in 𝒫 {Base}_{M})$
85	84	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})$
86	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)$
87	86 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)$
88	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}} ((z \in (S ∖ \{X\}) ⟼ G (z) \cdot_{M} z))$
89	88 6	breqtrrdi	$⊢ ((M \in LMod \land S ∖ \{X\} \in 𝒫 {Base}_{M}) \land G \in (E^{(S ∖ \{X\})}) \land {finSupp}_{0_{R}} (G)) \to {finSupp}_{Z} ((z \in (S ∖ \{X\}) ⟼ G (z) \cdot_{M} z))$
90	85 66 87 89	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}_{Z} ((z \in (S ∖ \{X\}) ⟼ G (z) \cdot_{M} z))$
91	1 2 3 6 47 48 11 51 63 82 90	gsumvsmul	$⊢ ((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{z \in S ∖ \{X\}}{\sum_{M}} (N (F (X)) \cdot_{M} (G (z) \cdot_{M} z)) = N (F (X)) \cdot_{M} (\underset{z \in S ∖ \{X\}}{\sum_{M}}, (G (z) \cdot_{M} z))$
92	33 46 91	3eqtr2rd	$⊢ ((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\})$

Metamath Proof Explorer

Theorem lincresunit3lem2

Proof