lincext3

Description: Property 3 of an extension of a linear combination. (Contributed by AV, 23-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	lincext.b	$⊢ B = {Base}_{M}$
	lincext.r	$⊢ R = Scalar (M)$
	lincext.e	$⊢ E = {Base}_{R}$
	lincext.0	$⊢ \underset{˙}{0} = 0_{R}$
	lincext.z	$⊢ Z = 0_{M}$
	lincext.n	$⊢ N = {inv}_{g} (R)$
	lincext.f	$⊢ F = (z \in S ⟼ if (z = X, N (Y), G (z)))$
Assertion	lincext3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to F linC (M) S = Z$

Proof

Step	Hyp	Ref	Expression
1		lincext.b	$⊢ B = {Base}_{M}$
2		lincext.r	$⊢ R = Scalar (M)$
3		lincext.e	$⊢ E = {Base}_{R}$
4		lincext.0	$⊢ \underset{˙}{0} = 0_{R}$
5		lincext.z	$⊢ Z = 0_{M}$
6		lincext.n	$⊢ N = {inv}_{g} (R)$
7		lincext.f	$⊢ F = (z \in S ⟼ if (z = X, N (Y), G (z)))$
8		simp1l	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to M \in LMod$
9		simp1r	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to S \in 𝒫 B$
10		simp2	$⊢ (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \to X \in S$
11	10	3ad2ant2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to X \in S$
12	1 2 3 4 5 6 7	lincext1	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to F \in (E^{S})$
13	12	3adant3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to F \in (E^{S})$
14	1 2 3 4 5 6 7	lincext2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land {finSupp}_{\underset{˙}{0}} (G)) \to {finSupp}_{\underset{˙}{0}} (F)$
15	14	3adant3r	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to {finSupp}_{\underset{˙}{0}} (F)$
16		elmapi	$⊢ G \in (E^{(S ∖ \{X\})}) \to G : S ∖ \{X\} ⟶ E$
17	7	fdmdifeqresdif	$⊢ G : S ∖ \{X\} ⟶ E \to G = {F ↾}_{(S ∖ \{X\})}$
18	16 17	syl	$⊢ G \in (E^{(S ∖ \{X\})}) \to G = {F ↾}_{(S ∖ \{X\})}$
19	18	3ad2ant3	$⊢ (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \to G = {F ↾}_{(S ∖ \{X\})}$
20	19	3ad2ant2	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to G = {F ↾}_{(S ∖ \{X\})}$
21		eqid	$⊢ \cdot_{M} = \cdot_{M}$
22		eqid	$⊢ +_{M} = +_{M}$
23	1 2 3 21 22 4	lincdifsn	$⊢ ((M \in LMod \land S \in 𝒫 B \land X \in S) \land (F \in (E^{S}) \land {finSupp}_{\underset{˙}{0}} (F)) \land G = {F ↾}_{(S ∖ \{X\})}) \to F linC (M) S = (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X)$
24	8 9 11 13 15 20 23	syl321anc	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to F linC (M) S = (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X)$
25		oveq1	$⊢ G linC (M) (S ∖ \{X\}) = Y \cdot_{M} X \to (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X)$
26	25	eqcoms	$⊢ Y \cdot_{M} X = G linC (M) (S ∖ \{X\}) \to (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X)$
27	26	adantl	$⊢ ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\})) \to (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X)$
28	27	3ad2ant3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X)$
29		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
30		simpll	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to M \in LMod$
31		elelpwi	$⊢ (X \in S \land S \in 𝒫 B) \to X \in B$
32	31	expcom	$⊢ S \in 𝒫 B \to (X \in S \to X \in B)$
33	32	adantl	$⊢ (M \in LMod \land S \in 𝒫 B) \to (X \in S \to X \in B)$
34	33	com12	$⊢ X \in S \to ((M \in LMod \land S \in 𝒫 B) \to X \in B)$
35	34	3ad2ant2	$⊢ (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \to ((M \in LMod \land S \in 𝒫 B) \to X \in B)$
36	35	impcom	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to X \in B$
37		simpr1	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to Y \in E$
38	1 2 21 29 3 6 30 36 37	lmodvsneg	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to {inv}_{g} (M) (Y \cdot_{M} X) = N (Y) \cdot_{M} X$
39		iftrue	$⊢ z = X \to if (z = X, N (Y), G (z)) = N (Y)$
40	10	adantl	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to X \in S$
41		fvexd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to N (Y) \in V$
42	7 39 40 41	fvmptd3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to F (X) = N (Y)$
43	42	eqcomd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to N (Y) = F (X)$
44	43	oveq1d	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to N (Y) \cdot_{M} X = F (X) \cdot_{M} X$
45	38 44	eqtr2d	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to F (X) \cdot_{M} X = {inv}_{g} (M) (Y \cdot_{M} X)$
46	45	oveq2d	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X) = (Y \cdot_{M} X) +_{M} {inv}_{g} (M) (Y \cdot_{M} X)$
47	1 2 21 3	lmodvscl	$⊢ (M \in LMod \land Y \in E \land X \in B) \to Y \cdot_{M} X \in B$
48	30 37 36 47	syl3anc	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to Y \cdot_{M} X \in B$
49	1 22 5 29	lmodvnegid	$⊢ (M \in LMod \land Y \cdot_{M} X \in B) \to (Y \cdot_{M} X) +_{M} {inv}_{g} (M) (Y \cdot_{M} X) = Z$
50	30 48 49	syl2anc	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to (Y \cdot_{M} X) +_{M} {inv}_{g} (M) (Y \cdot_{M} X) = Z$
51	46 50	eqtrd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X) = Z$
52	51	3adant3	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to (Y \cdot_{M} X) +_{M} (F (X) \cdot_{M} X) = Z$
53	28 52	eqtrd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to (G linC (M) (S ∖ \{X\})) +_{M} (F (X) \cdot_{M} X) = Z$
54	24 53	eqtrd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (G) \land Y \cdot_{M} X = G linC (M) (S ∖ \{X\}))) \to F linC (M) S = Z$

Metamath Proof Explorer

Theorem lincext3

Proof