lincreslvec3

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	lincreslvec3	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \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		lveclmod	$⊢ M \in LVec \to M \in LMod$
12	11	3anim2i	$⊢ (S \in 𝒫 B \land M \in LVec \land X \in S) \to (S \in 𝒫 B \land M \in LMod \land X \in S)$
13	12	3ad2ant1	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \land F linC (M) S = Z) \to (S \in 𝒫 B \land M \in LMod \land X \in S)$
14		simp21	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \land F linC (M) S = Z) \to F \in (E^{S})$
15		elmapi	$⊢ F \in (E^{S}) \to F : S ⟶ E$
16	15	3ad2ant1	$⊢ (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \to F : S ⟶ E$
17		simp3	$⊢ (S \in 𝒫 B \land M \in LVec \land X \in S) \to X \in S$
18		ffvelrn	$⊢ (F : S ⟶ E \land X \in S) \to F (X) \in E$
19	16 17 18	syl2anr	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F))) \to F (X) \in E$
20		simpr2	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F))) \to F (X) \neq \underset{˙}{0}$
21	2	lvecdrng	$⊢ M \in LVec \to R \in DivRing$
22	21	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LVec \land X \in S) \to R \in DivRing$
23	22	adantr	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F))) \to R \in DivRing$
24	3 4 5	drngunit	$⊢ R \in DivRing \to (F (X) \in U \leftrightarrow (F (X) \in E \land F (X) \neq \underset{˙}{0}))$
25	23 24	syl	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F))) \to (F (X) \in U \leftrightarrow (F (X) \in E \land F (X) \neq \underset{˙}{0}))$
26	19 20 25	mpbir2and	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F))) \to F (X) \in U$
27	26	3adant3	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \land F linC (M) S = Z) \to F (X) \in U$
28		simp3	$⊢ (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \to {finSupp}_{\underset{˙}{0}} (F)$
29	28	3ad2ant2	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \land F linC (M) S = Z) \to {finSupp}_{\underset{˙}{0}} (F)$
30		simp3	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \land F linC (M) S = Z) \to F linC (M) S = Z$
31	1 2 3 4 5 6 7 8 9 10	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$
32	13 14 27 29 30 31	syl131anc	$⊢ ((S \in 𝒫 B \land M \in LVec \land X \in S) \land (F \in (E^{S}) \land F (X) \neq \underset{˙}{0} \land {finSupp}_{\underset{˙}{0}} (F)) \land F linC (M) S = Z) \to G linC (M) (S ∖ \{X\}) = X$

Metamath Proof Explorer

Theorem lincreslvec3

Proof