issubassa3

Description: A subring that is also a subspace is a subalgebra. The key theorem is islss3 . (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	issubassa.s	$⊢ S = W ↾_{𝑠} A$
	issubassa.l	$⊢ L = LSubSp (W)$
Assertion	issubassa3	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to S \in AssAlg$

Proof

Step	Hyp	Ref	Expression
1		issubassa.s	$⊢ S = W ↾_{𝑠} A$
2		issubassa.l	$⊢ L = LSubSp (W)$
3	1	subrgbas	$⊢ A \in SubRing (W) \to A = {Base}_{S}$
4	3	ad2antrl	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to A = {Base}_{S}$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6	1 5	resssca	$⊢ A \in SubRing (W) \to Scalar (W) = Scalar (S)$
7	6	ad2antrl	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to Scalar (W) = Scalar (S)$
8		eqidd	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
9		eqid	$⊢ \cdot_{W} = \cdot_{W}$
10	1 9	ressvsca	$⊢ A \in SubRing (W) \to \cdot_{W} = \cdot_{S}$
11	10	ad2antrl	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to \cdot_{W} = \cdot_{S}$
12		eqid	$⊢ \cdot_{W} = \cdot_{W}$
13	1 12	ressmulr	$⊢ A \in SubRing (W) \to \cdot_{W} = \cdot_{S}$
14	13	ad2antrl	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to \cdot_{W} = \cdot_{S}$
15		assalmod	$⊢ W \in AssAlg \to W \in LMod$
16		simpr	$⊢ (A \in SubRing (W) \land A \in L) \to A \in L$
17	1 2	lsslmod	$⊢ (W \in LMod \land A \in L) \to S \in LMod$
18	15 16 17	syl2an	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to S \in LMod$
19	1	subrgring	$⊢ A \in SubRing (W) \to S \in Ring$
20	19	ad2antrl	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to S \in Ring$
21		idd	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to (x \in {Base}_{Scalar (W)} \to x \in {Base}_{Scalar (W)})$
22		eqid	$⊢ {Base}_{W} = {Base}_{W}$
23	22	subrgss	$⊢ A \in SubRing (W) \to A \subseteq {Base}_{W}$
24	23	ad2antrl	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to A \subseteq {Base}_{W}$
25	24	sseld	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to (y \in A \to y \in {Base}_{W})$
26	24	sseld	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to (z \in A \to z \in {Base}_{W})$
27	21 25 26	3anim123d	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to ((x \in {Base}_{Scalar (W)} \land y \in A \land z \in A) \to (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W} \land z \in {Base}_{W}))$
28	27	imp	$⊢ ((W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \land (x \in {Base}_{Scalar (W)} \land y \in A \land z \in A)) \to (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W} \land z \in {Base}_{W})$
29		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
30	22 5 29 9 12	assaass	$⊢ (W \in AssAlg \land (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x \cdot_{W} y) \cdot_{W} z = x \cdot_{W} (y \cdot_{W} z)$
31	30	adantlr	$⊢ ((W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \land (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x \cdot_{W} y) \cdot_{W} z = x \cdot_{W} (y \cdot_{W} z)$
32	28 31	syldan	$⊢ ((W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \land (x \in {Base}_{Scalar (W)} \land y \in A \land z \in A)) \to (x \cdot_{W} y) \cdot_{W} z = x \cdot_{W} (y \cdot_{W} z)$
33	22 5 29 9 12	assaassr	$⊢ (W \in AssAlg \land (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to y \cdot_{W} (x \cdot_{W} z) = x \cdot_{W} (y \cdot_{W} z)$
34	33	adantlr	$⊢ ((W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \land (x \in {Base}_{Scalar (W)} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to y \cdot_{W} (x \cdot_{W} z) = x \cdot_{W} (y \cdot_{W} z)$
35	28 34	syldan	$⊢ ((W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \land (x \in {Base}_{Scalar (W)} \land y \in A \land z \in A)) \to y \cdot_{W} (x \cdot_{W} z) = x \cdot_{W} (y \cdot_{W} z)$
36	4 7 8 11 14 18 20 32 35	isassad	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to S \in AssAlg$

Metamath Proof Explorer

Theorem issubassa3

Proof