lincext1

Description: Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 29-Apr-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	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})$

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		eqid	$⊢ Scalar (M) = Scalar (M)$
9	8	lmodfgrp	$⊢ M \in LMod \to Scalar (M) \in Grp$
10	9	ad2antrr	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to Scalar (M) \in Grp$
11	2 10	eqeltrid	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to R \in Grp$
12		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$
13	3 6	grpinvcl	$⊢ (R \in Grp \land Y \in E) \to N (Y) \in E$
14	11 12 13	syl2anc	$⊢ ((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 E$
15	14	ad2antrr	$⊢ ((((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \land z \in S) \land z = X) \to N (Y) \in E$
16		elmapi	$⊢ G \in (E^{(S ∖ \{X\})}) \to G : S ∖ \{X\} ⟶ E$
17		df-ne	$⊢ z \neq X \leftrightarrow \neg z = X$
18	17	biimpri	$⊢ \neg z = X \to z \neq X$
19	18	anim2i	$⊢ (z \in S \land \neg z = X) \to (z \in S \land z \neq X)$
20		eldifsn	$⊢ z \in (S ∖ \{X\}) \leftrightarrow (z \in S \land z \neq X)$
21	19 20	sylibr	$⊢ (z \in S \land \neg z = X) \to z \in (S ∖ \{X\})$
22		ffvelrn	$⊢ (G : S ∖ \{X\} ⟶ E \land z \in (S ∖ \{X\})) \to G (z) \in E$
23	21 22	sylan2	$⊢ (G : S ∖ \{X\} ⟶ E \land (z \in S \land \neg z = X)) \to G (z) \in E$
24	23	ex	$⊢ G : S ∖ \{X\} ⟶ E \to ((z \in S \land \neg z = X) \to G (z) \in E)$
25	16 24	syl	$⊢ G \in (E^{(S ∖ \{X\})}) \to ((z \in S \land \neg z = X) \to G (z) \in E)$
26	25	3ad2ant3	$⊢ (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})})) \to ((z \in S \land \neg z = X) \to G (z) \in E)$
27	26	adantl	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to ((z \in S \land \neg z = X) \to G (z) \in E)$
28	27	impl	$⊢ ((((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \land z \in S) \land \neg z = X) \to G (z) \in E$
29	15 28	ifclda	$⊢ (((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \land z \in S) \to if (z = X, N (Y), G (z)) \in E$
30	29	fmpttd	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to (z \in S ⟼ if (z = X, N (Y), G (z))) : S ⟶ E$
31		simpr	$⊢ (M \in LMod \land S \in 𝒫 B) \to S \in 𝒫 B$
32	3	fvexi	$⊢ E \in V$
33	31 32	jctil	$⊢ (M \in LMod \land S \in 𝒫 B) \to (E \in V \land S \in 𝒫 B)$
34	33	adantr	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to (E \in V \land S \in 𝒫 B)$
35		elmapg	$⊢ (E \in V \land S \in 𝒫 B) \to ((z \in S ⟼ if (z = X, N (Y), G (z))) \in (E^{S}) \leftrightarrow (z \in S ⟼ if (z = X, N (Y), G (z))) : S ⟶ E)$
36	34 35	syl	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to ((z \in S ⟼ if (z = X, N (Y), G (z))) \in (E^{S}) \leftrightarrow (z \in S ⟼ if (z = X, N (Y), G (z))) : S ⟶ E)$
37	30 36	mpbird	$⊢ ((M \in LMod \land S \in 𝒫 B) \land (Y \in E \land X \in S \land G \in (E^{(S ∖ \{X\})}))) \to (z \in S ⟼ if (z = X, N (Y), G (z))) \in (E^{S})$
38	7 37	eqeltrid	$⊢ ((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})$

Metamath Proof Explorer

Theorem lincext1

Proof