lincresunitlem2

Description: Lemma 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	lincresunitlem2	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land Y \in S) \to I (N (F (X))) \underset{˙}{\cdot} F (Y) \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	13	adantr	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land Y \in S) \to R \in Ring$
15	1 2 3 4 5 6 7 8 9 10	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$
16	15	adantr	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land Y \in S) \to I (N (F (X))) \in E$
17		elmapi	$⊢ F \in (E^{S}) \to F : S ⟶ E$
18		ffvelrn	$⊢ (F : S ⟶ E \land Y \in S) \to F (Y) \in E$
19	18	ex	$⊢ F : S ⟶ E \to (Y \in S \to F (Y) \in E)$
20	17 19	syl	$⊢ F \in (E^{S}) \to (Y \in S \to F (Y) \in E)$
21	20	ad2antrl	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \to (Y \in S \to F (Y) \in E)$
22	21	imp	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land Y \in S) \to F (Y) \in E$
23	3 9	ringcl	$⊢ (R \in Ring \land I (N (F (X))) \in E \land F (Y) \in E) \to I (N (F (X))) \underset{˙}{\cdot} F (Y) \in E$
24	14 16 22 23	syl3anc	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land Y \in S) \to I (N (F (X))) \underset{˙}{\cdot} F (Y) \in E$

Metamath Proof Explorer

Theorem lincresunitlem2

Proof