aspid

Description: The algebraic span of a subalgebra is itself. ( spanid analog.) (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	$⊢ A = AlgSpan (W)$
	aspval.v	$⊢ V = {Base}_{W}$
	aspval.l	$⊢ L = LSubSp (W)$
Assertion	aspid	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to A (S) = S$

Step	Hyp	Ref	Expression
1		aspval.a	$⊢ A = AlgSpan (W)$
2		aspval.v	$⊢ V = {Base}_{W}$
3		aspval.l	$⊢ L = LSubSp (W)$
4		simp1	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to W \in AssAlg$
5	2	subrgss	$⊢ S \in SubRing (W) \to S \subseteq V$
6	5	3ad2ant2	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to S \subseteq V$
7	1 2 3	aspval	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$
8	4 6 7	syl2anc	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to A (S) = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$
9		3simpc	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to (S \in SubRing (W) \land S \in L)$
10		elin	$⊢ S \in (SubRing (W) \cap L) \leftrightarrow (S \in SubRing (W) \land S \in L)$
11	9 10	sylibr	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to S \in (SubRing (W) \cap L)$
12		intmin	$⊢ S \in (SubRing (W) \cap L) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} = S$
13	11 12	syl	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} = S$
14	8 13	eqtrd	$⊢ (W \in AssAlg \land S \in SubRing (W) \land S \in L) \to A (S) = S$

Metamath Proof Explorer