Metamath Proof Explorer

Theorem lincresunitlem1

Description: Lemma 1 for properties 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	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$

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	2	lmodring	$⊢ M \in LMod \to R \in Ring$
12	11	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to R \in Ring$
13	12	adantr	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \to R \in Ring$
14		simpr	$⊢ (F \in (E^{S}) \land F (X) \in U) \to F (X) \in U$
15	4 7	unitnegcl	$⊢ (R \in Ring \land F (X) \in U) \to N (F (X)) \in U$
16	12 14 15	syl2an	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \to N (F (X)) \in U$
17	4 8 3	ringinvcl	$⊢ (R \in Ring \land N (F (X)) \in U) \to I (N (F (X))) \in E$
18	13 16 17	syl2anc	$⊢ ((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$