issubassa2

Description: A subring of a unital algebra is a subspace and thus a subalgebra iff it contains all scalar multiples of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	issubassa2.a	$⊢ A = algSc (W)$
	issubassa2.l	$⊢ L = LSubSp (W)$
Assertion	issubassa2	$⊢ (W \in AssAlg \land S \in SubRing (W)) \to (S \in L \leftrightarrow ran A \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		issubassa2.a	$⊢ A = algSc (W)$
2		issubassa2.l	$⊢ L = LSubSp (W)$
3		eqid	$⊢ 1_{W} = 1_{W}$
4		eqid	$⊢ LSpan (W) = LSpan (W)$
5	1 3 4	rnascl	$⊢ W \in AssAlg \to ran A = LSpan (W) (\{1_{W}\})$
6	5	ad2antrr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land S \in L) \to ran A = LSpan (W) (\{1_{W}\})$
7		assalmod	$⊢ W \in AssAlg \to W \in LMod$
8	7	ad2antrr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land S \in L) \to W \in LMod$
9		simpr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land S \in L) \to S \in L$
10	3	subrg1cl	$⊢ S \in SubRing (W) \to 1_{W} \in S$
11	10	ad2antlr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land S \in L) \to 1_{W} \in S$
12	2 4 8 9 11	ellspsn5	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land S \in L) \to LSpan (W) (\{1_{W}\}) \subseteq S$
13	6 12	eqsstrd	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land S \in L) \to ran A \subseteq S$
14		subrgsubg	$⊢ S \in SubRing (W) \to S \in SubGrp (W)$
15	14	ad2antlr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \to S \in SubGrp (W)$
16		simplll	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to W \in AssAlg$
17		simprl	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to x \in {Base}_{Scalar (W)}$
18		eqid	$⊢ {Base}_{W} = {Base}_{W}$
19	18	subrgss	$⊢ S \in SubRing (W) \to S \subseteq {Base}_{W}$
20	19	ad2antlr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \to S \subseteq {Base}_{W}$
21	20	sselda	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land y \in S) \to y \in {Base}_{W}$
22	21	adantrl	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to y \in {Base}_{W}$
23		eqid	$⊢ Scalar (W) = Scalar (W)$
24		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
25		eqid	$⊢ \cdot_{W} = \cdot_{W}$
26		eqid	$⊢ \cdot_{W} = \cdot_{W}$
27	1 23 24 18 25 26	asclmul1	$⊢ (W \in AssAlg \land x \in {Base}_{Scalar (W)} \land y \in {Base}_{W}) \to A (x) \cdot_{W} y = x \cdot_{W} y$
28	16 17 22 27	syl3anc	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to A (x) \cdot_{W} y = x \cdot_{W} y$
29		simpllr	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to S \in SubRing (W)$
30		simplr	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land x \in {Base}_{Scalar (W)}) \to ran A \subseteq S$
31	1 23 24	asclfn	$⊢ A Fn {Base}_{Scalar (W)}$
32	31	a1i	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \to A Fn {Base}_{Scalar (W)}$
33		fnfvelrn	$⊢ (A Fn {Base}_{Scalar (W)} \land x \in {Base}_{Scalar (W)}) \to A (x) \in ran A$
34	32 33	sylan	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land x \in {Base}_{Scalar (W)}) \to A (x) \in ran A$
35	30 34	sseldd	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land x \in {Base}_{Scalar (W)}) \to A (x) \in S$
36	35	adantrr	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to A (x) \in S$
37		simprr	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to y \in S$
38	25	subrgmcl	$⊢ (S \in SubRing (W) \land A (x) \in S \land y \in S) \to A (x) \cdot_{W} y \in S$
39	29 36 37 38	syl3anc	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to A (x) \cdot_{W} y \in S$
40	28 39	eqeltrrd	$⊢ (((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \land (x \in {Base}_{Scalar (W)} \land y \in S)) \to x \cdot_{W} y \in S$
41	40	ralrimivva	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \to \forall x \in {Base}_{Scalar (W)} \forall y \in S x \cdot_{W} y \in S$
42	23 24 18 26 2	islss4	$⊢ W \in LMod \to (S \in L \leftrightarrow (S \in SubGrp (W) \land \forall x \in {Base}_{Scalar (W)} \forall y \in S x \cdot_{W} y \in S))$
43	7 42	syl	$⊢ W \in AssAlg \to (S \in L \leftrightarrow (S \in SubGrp (W) \land \forall x \in {Base}_{Scalar (W)} \forall y \in S x \cdot_{W} y \in S))$
44	43	ad2antrr	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \to (S \in L \leftrightarrow (S \in SubGrp (W) \land \forall x \in {Base}_{Scalar (W)} \forall y \in S x \cdot_{W} y \in S))$
45	15 41 44	mpbir2and	$⊢ ((W \in AssAlg \land S \in SubRing (W)) \land ran A \subseteq S) \to S \in L$
46	13 45	impbida	$⊢ (W \in AssAlg \land S \in SubRing (W)) \to (S \in L \leftrightarrow ran A \subseteq S)$

Metamath Proof Explorer

Theorem issubassa2

Proof