This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aspss

Description: Span preserves subset ordering. ( spanss analog.) (Contributed by Mario Carneiro, 7-Jan-2015)

		Ref	Expression
	Hypotheses	aspval.a	$⊢ A = AlgSpan (W)$
		aspval.v	$⊢ V = {Base}_{W}$
	Assertion	aspss	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to A (T) \subseteq A (S)$

Proof

Step	Hyp	Ref	Expression
1		aspval.a	$⊢ A = AlgSpan (W)$
2		aspval.v	$⊢ V = {Base}_{W}$
3		simpl3	$⊢ ((W \in AssAlg \land S \subseteq V \land T \subseteq S) \land t \in (SubRing (W) \cap LSubSp (W))) \to T \subseteq S$
4		sstr2	$⊢ T \subseteq S \to (S \subseteq t \to T \subseteq t)$
5	3 4	syl	$⊢ ((W \in AssAlg \land S \subseteq V \land T \subseteq S) \land t \in (SubRing (W) \cap LSubSp (W))) \to (S \subseteq t \to T \subseteq t)$
6	5	ss2rabdv	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \subseteq \{t \in (SubRing (W) \cap LSubSp (W)) \| T \subseteq t\}$
7		intss	$⊢ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \subseteq \{t \in (SubRing (W) \cap LSubSp (W)) \| T \subseteq t\} \to ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| T \subseteq t\} \subseteq ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\}$
8	6 7	syl	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| T \subseteq t\} \subseteq ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\}$
9		simp1	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to W \in AssAlg$
10		simp3	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to T \subseteq S$
11		simp2	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to S \subseteq V$
12	10 11	sstrd	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to T \subseteq V$
13		eqid	$⊢ LSubSp (W) = LSubSp (W)$
14	1 2 13	aspval	$⊢ (W \in AssAlg \land T \subseteq V) \to A (T) = ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| T \subseteq t\}$
15	9 12 14	syl2anc	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to A (T) = ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| T \subseteq t\}$
16	1 2 13	aspval	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\}$
17	16	3adant3	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to A (S) = ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\}$
18	8 15 17	3sstr4d	$⊢ (W \in AssAlg \land S \subseteq V \land T \subseteq S) \to A (T) \subseteq A (S)$