lmhmlsp

Description: Homomorphisms preserve spans. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lmhmlsp.v	$⊢ V = {Base}_{S}$
	lmhmlsp.k	$⊢ K = LSpan (S)$
	lmhmlsp.l	$⊢ L = LSpan (T)$
Assertion	lmhmlsp	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [K (U)] = L (F [U])$

Proof

Step	Hyp	Ref	Expression
1		lmhmlsp.v	$⊢ V = {Base}_{S}$
2		lmhmlsp.k	$⊢ K = LSpan (S)$
3		lmhmlsp.l	$⊢ L = LSpan (T)$
4		eqid	$⊢ {Base}_{T} = {Base}_{T}$
5	1 4	lmhmf	$⊢ F \in (S LMHom T) \to F : V ⟶ {Base}_{T}$
6	5	adantr	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F : V ⟶ {Base}_{T}$
7	6	ffund	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to Fun F$
8		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
9	8	adantr	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to S \in LMod$
10		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
11	10	adantr	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to T \in LMod$
12		imassrn	$⊢ F [U] \subseteq ran F$
13	6	frnd	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to ran F \subseteq {Base}_{T}$
14	12 13	sstrid	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [U] \subseteq {Base}_{T}$
15		eqid	$⊢ LSubSp (T) = LSubSp (T)$
16	4 15 3	lspcl	$⊢ (T \in LMod \land F [U] \subseteq {Base}_{T}) \to L (F [U]) \in LSubSp (T)$
17	11 14 16	syl2anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to L (F [U]) \in LSubSp (T)$
18		eqid	$⊢ LSubSp (S) = LSubSp (S)$
19	18 15	lmhmpreima	$⊢ (F \in (S LMHom T) \land L (F [U]) \in LSubSp (T)) \to F^{-1} [L (F [U])] \in LSubSp (S)$
20	17 19	syldan	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F^{-1} [L (F [U])] \in LSubSp (S)$
21		incom	$⊢ dom F \cap U = U \cap dom F$
22		simpr	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U \subseteq V$
23	6	fdmd	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to dom F = V$
24	22 23	sseqtrrd	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U \subseteq dom F$
25		df-ss	$⊢ U \subseteq dom F \leftrightarrow U \cap dom F = U$
26	24 25	sylib	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U \cap dom F = U$
27	21 26	eqtr2id	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U = dom F \cap U$
28		dminss	$⊢ dom F \cap U \subseteq F^{-1} [F [U]]$
29	27 28	eqsstrdi	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U \subseteq F^{-1} [F [U]]$
30	4 3	lspssid	$⊢ (T \in LMod \land F [U] \subseteq {Base}_{T}) \to F [U] \subseteq L (F [U])$
31	11 14 30	syl2anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [U] \subseteq L (F [U])$
32		imass2	$⊢ F [U] \subseteq L (F [U]) \to F^{-1} [F [U]] \subseteq F^{-1} [L (F [U])]$
33	31 32	syl	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F^{-1} [F [U]] \subseteq F^{-1} [L (F [U])]$
34	29 33	sstrd	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U \subseteq F^{-1} [L (F [U])]$
35	18 2	lspssp	$⊢ (S \in LMod \land F^{-1} [L (F [U])] \in LSubSp (S) \land U \subseteq F^{-1} [L (F [U])]) \to K (U) \subseteq F^{-1} [L (F [U])]$
36	9 20 34 35	syl3anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to K (U) \subseteq F^{-1} [L (F [U])]$
37		funimass2	$⊢ (Fun F \land K (U) \subseteq F^{-1} [L (F [U])]) \to F [K (U)] \subseteq L (F [U])$
38	7 36 37	syl2anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [K (U)] \subseteq L (F [U])$
39	1 18 2	lspcl	$⊢ (S \in LMod \land U \subseteq V) \to K (U) \in LSubSp (S)$
40	9 22 39	syl2anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to K (U) \in LSubSp (S)$
41	18 15	lmhmima	$⊢ (F \in (S LMHom T) \land K (U) \in LSubSp (S)) \to F [K (U)] \in LSubSp (T)$
42	40 41	syldan	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [K (U)] \in LSubSp (T)$
43	1 2	lspssid	$⊢ (S \in LMod \land U \subseteq V) \to U \subseteq K (U)$
44	9 22 43	syl2anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to U \subseteq K (U)$
45		imass2	$⊢ U \subseteq K (U) \to F [U] \subseteq F [K (U)]$
46	44 45	syl	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [U] \subseteq F [K (U)]$
47	15 3	lspssp	$⊢ (T \in LMod \land F [K (U)] \in LSubSp (T) \land F [U] \subseteq F [K (U)]) \to L (F [U]) \subseteq F [K (U)]$
48	11 42 46 47	syl3anc	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to L (F [U]) \subseteq F [K (U)]$
49	38 48	eqssd	$⊢ (F \in (S LMHom T) \land U \subseteq V) \to F [K (U)] = L (F [U])$

Metamath Proof Explorer

Theorem lmhmlsp

Proof