lspextmo

Description: A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015) (Revised by NM, 17-Jun-2017)

	Ref	Expression
Hypotheses	lspextmo.b	$⊢ B = {Base}_{S}$
	lspextmo.k	$⊢ K = LSpan (S)$
Assertion	lspextmo	$⊢ (X \subseteq B \land K (X) = B) \to \exists^{*} g \in (S LMHom T) {g ↾}_{X} = F$

Proof

Step	Hyp	Ref	Expression
1		lspextmo.b	$⊢ B = {Base}_{S}$
2		lspextmo.k	$⊢ K = LSpan (S)$
3		eqtr3	$⊢ ({g ↾}_{X} = F \land {h ↾}_{X} = F) \to {g ↾}_{X} = {h ↾}_{X}$
4		inss1	$⊢ g \cap h \subseteq g$
5		dmss	$⊢ g \cap h \subseteq g \to dom (g \cap h) \subseteq dom g$
6	4 5	ax-mp	$⊢ dom (g \cap h) \subseteq dom g$
7		eqid	$⊢ {Base}_{T} = {Base}_{T}$
8	1 7	lmhmf	$⊢ g \in (S LMHom T) \to g : B ⟶ {Base}_{T}$
9	8	ad2antrl	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to g : B ⟶ {Base}_{T}$
10	9	ffnd	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to g Fn B$
11	10	adantrr	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to g Fn B$
12	11	fndmd	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to dom g = B$
13	6 12	sseqtrid	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to dom (g \cap h) \subseteq B$
14		simplr	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to K (X) = B$
15		lmhmlmod1	$⊢ g \in (S LMHom T) \to S \in LMod$
16	15	adantr	$⊢ (g \in (S LMHom T) \land h \in (S LMHom T)) \to S \in LMod$
17	16	ad2antrl	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to S \in LMod$
18		eqid	$⊢ LSubSp (S) = LSubSp (S)$
19	18	lmhmeql	$⊢ (g \in (S LMHom T) \land h \in (S LMHom T)) \to dom (g \cap h) \in LSubSp (S)$
20	19	ad2antrl	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to dom (g \cap h) \in LSubSp (S)$
21		simprr	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to X \subseteq dom (g \cap h)$
22	18 2	lspssp	$⊢ (S \in LMod \land dom (g \cap h) \in LSubSp (S) \land X \subseteq dom (g \cap h)) \to K (X) \subseteq dom (g \cap h)$
23	17 20 21 22	syl3anc	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to K (X) \subseteq dom (g \cap h)$
24	14 23	eqsstrrd	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to B \subseteq dom (g \cap h)$
25	13 24	eqssd	$⊢ ((X \subseteq B \land K (X) = B) \land ((g \in (S LMHom T) \land h \in (S LMHom T)) \land X \subseteq dom (g \cap h))) \to dom (g \cap h) = B$
26	25	expr	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to (X \subseteq dom (g \cap h) \to dom (g \cap h) = B)$
27		simprr	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to h \in (S LMHom T)$
28	1 7	lmhmf	$⊢ h \in (S LMHom T) \to h : B ⟶ {Base}_{T}$
29		ffn	$⊢ h : B ⟶ {Base}_{T} \to h Fn B$
30	27 28 29	3syl	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to h Fn B$
31		simpll	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to X \subseteq B$
32		fnreseql	$⊢ (g Fn B \land h Fn B \land X \subseteq B) \to ({g ↾}_{X} = {h ↾}_{X} \leftrightarrow X \subseteq dom (g \cap h))$
33	10 30 31 32	syl3anc	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to ({g ↾}_{X} = {h ↾}_{X} \leftrightarrow X \subseteq dom (g \cap h))$
34		fneqeql	$⊢ (g Fn B \land h Fn B) \to (g = h \leftrightarrow dom (g \cap h) = B)$
35	10 30 34	syl2anc	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to (g = h \leftrightarrow dom (g \cap h) = B)$
36	26 33 35	3imtr4d	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to ({g ↾}_{X} = {h ↾}_{X} \to g = h)$
37	3 36	syl5	$⊢ ((X \subseteq B \land K (X) = B) \land (g \in (S LMHom T) \land h \in (S LMHom T))) \to (({g ↾}_{X} = F \land {h ↾}_{X} = F) \to g = h)$
38	37	ralrimivva	$⊢ (X \subseteq B \land K (X) = B) \to \forall g \in (S LMHom T) \forall h \in (S LMHom T) (({g ↾}_{X} = F \land {h ↾}_{X} = F) \to g = h)$
39		reseq1	$⊢ g = h \to {g ↾}_{X} = {h ↾}_{X}$
40	39	eqeq1d	$⊢ g = h \to ({g ↾}_{X} = F \leftrightarrow {h ↾}_{X} = F)$
41	40	rmo4	$⊢ \exists^{*} g \in (S LMHom T) {g ↾}_{X} = F \leftrightarrow \forall g \in (S LMHom T) \forall h \in (S LMHom T) (({g ↾}_{X} = F \land {h ↾}_{X} = F) \to g = h)$
42	38 41	sylibr	$⊢ (X \subseteq B \land K (X) = B) \to \exists^{*} g \in (S LMHom T) {g ↾}_{X} = F$

Metamath Proof Explorer

Theorem lspextmo

Proof