issubassa

Description: The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	issubassa.s	$⊢ S = W ↾_{𝑠} A$
	issubassa.l	$⊢ L = LSubSp (W)$
	issubassa.v	$⊢ V = {Base}_{W}$
	issubassa.o	$⊢ \underset{˙}{1} = 1_{W}$
Assertion	issubassa	$⊢ (W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \to (S \in AssAlg \leftrightarrow (A \in SubRing (W) \land A \in L))$

Proof

Step	Hyp	Ref	Expression
1		issubassa.s	$⊢ S = W ↾_{𝑠} A$
2		issubassa.l	$⊢ L = LSubSp (W)$
3		issubassa.v	$⊢ V = {Base}_{W}$
4		issubassa.o	$⊢ \underset{˙}{1} = 1_{W}$
5		simpl1	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to W \in AssAlg$
6		assaring	$⊢ W \in AssAlg \to W \in Ring$
7	5 6	syl	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to W \in Ring$
8		assaring	$⊢ S \in AssAlg \to S \in Ring$
9	8	adantl	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to S \in Ring$
10	1 9	eqeltrrid	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to W ↾_{𝑠} A \in Ring$
11		simpl3	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to A \subseteq V$
12		simpl2	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to \underset{˙}{1} \in A$
13	11 12	jca	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to (A \subseteq V \land \underset{˙}{1} \in A)$
14	3 4	issubrg	$⊢ A \in SubRing (W) \leftrightarrow ((W \in Ring \land W ↾_{𝑠} A \in Ring) \land (A \subseteq V \land \underset{˙}{1} \in A))$
15	7 10 13 14	syl21anbrc	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to A \in SubRing (W)$
16		assalmod	$⊢ S \in AssAlg \to S \in LMod$
17	16	adantl	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to S \in LMod$
18		assalmod	$⊢ W \in AssAlg \to W \in LMod$
19	1 3 2	islss3	$⊢ W \in LMod \to (A \in L \leftrightarrow (A \subseteq V \land S \in LMod))$
20	5 18 19	3syl	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to (A \in L \leftrightarrow (A \subseteq V \land S \in LMod))$
21	11 17 20	mpbir2and	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to A \in L$
22	15 21	jca	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land S \in AssAlg) \to (A \in SubRing (W) \land A \in L)$
23	1 2	issubassa3	$⊢ (W \in AssAlg \land (A \in SubRing (W) \land A \in L)) \to S \in AssAlg$
24	23	3ad2antl1	$⊢ ((W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \land (A \in SubRing (W) \land A \in L)) \to S \in AssAlg$
25	22 24	impbida	$⊢ (W \in AssAlg \land \underset{˙}{1} \in A \land A \subseteq V) \to (S \in AssAlg \leftrightarrow (A \in SubRing (W) \land A \in L))$

Metamath Proof Explorer

Theorem issubassa

Proof