sralmod

Description: The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014)

		Ref	Expression
	Hypothesis	sralmod.a	$⊢ A = subringAlg (W) (S)$
	Assertion	sralmod	$⊢ S \in SubRing (W) \to A \in LMod$

Proof

Step	Hyp	Ref	Expression
1		sralmod.a	$⊢ A = subringAlg (W) (S)$
2	1	a1i	$⊢ S \in SubRing (W) \to A = subringAlg (W) (S)$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	3	subrgss	$⊢ S \in SubRing (W) \to S \subseteq {Base}_{W}$
5	2 4	srabase	$⊢ S \in SubRing (W) \to {Base}_{W} = {Base}_{A}$
6	2 4	sraaddg	$⊢ S \in SubRing (W) \to +_{W} = +_{A}$
7	2 4	srasca	$⊢ S \in SubRing (W) \to W ↾_{𝑠} S = Scalar (A)$
8	2 4	sravsca	$⊢ S \in SubRing (W) \to \cdot_{W} = \cdot_{A}$
9		eqid	$⊢ W ↾_{𝑠} S = W ↾_{𝑠} S$
10	9 3	ressbas	$⊢ S \in SubRing (W) \to S \cap {Base}_{W} = {Base}_{(W ↾_{𝑠} S)}$
11		eqid	$⊢ +_{W} = +_{W}$
12	9 11	ressplusg	$⊢ S \in SubRing (W) \to +_{W} = +_{(W ↾_{𝑠} S)}$
13		eqid	$⊢ \cdot_{W} = \cdot_{W}$
14	9 13	ressmulr	$⊢ S \in SubRing (W) \to \cdot_{W} = \cdot_{(W ↾_{𝑠} S)}$
15		eqid	$⊢ 1_{W} = 1_{W}$
16	9 15	subrg1	$⊢ S \in SubRing (W) \to 1_{W} = 1_{(W ↾_{𝑠} S)}$
17	9	subrgring	$⊢ S \in SubRing (W) \to W ↾_{𝑠} S \in Ring$
18		subrgrcl	$⊢ S \in SubRing (W) \to W \in Ring$
19		ringgrp	$⊢ W \in Ring \to W \in Grp$
20	18 19	syl	$⊢ S \in SubRing (W) \to W \in Grp$
21		eqidd	$⊢ S \in SubRing (W) \to {Base}_{W} = {Base}_{W}$
22	6	oveqdr	$⊢ (S \in SubRing (W) \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to x +_{W} y = x +_{A} y$
23	21 5 22	grppropd	$⊢ S \in SubRing (W) \to (W \in Grp \leftrightarrow A \in Grp)$
24	20 23	mpbid	$⊢ S \in SubRing (W) \to A \in Grp$
25	18	3ad2ant1	$⊢ (S \in SubRing (W) \land x \in (S \cap {Base}_{W}) \land y \in {Base}_{W}) \to W \in Ring$
26		elinel2	$⊢ x \in (S \cap {Base}_{W}) \to x \in {Base}_{W}$
27	26	3ad2ant2	$⊢ (S \in SubRing (W) \land x \in (S \cap {Base}_{W}) \land y \in {Base}_{W}) \to x \in {Base}_{W}$
28		simp3	$⊢ (S \in SubRing (W) \land x \in (S \cap {Base}_{W}) \land y \in {Base}_{W}) \to y \in {Base}_{W}$
29	3 13	ringcl	$⊢ (W \in Ring \land x \in {Base}_{W} \land y \in {Base}_{W}) \to x \cdot_{W} y \in {Base}_{W}$
30	25 27 28 29	syl3anc	$⊢ (S \in SubRing (W) \land x \in (S \cap {Base}_{W}) \land y \in {Base}_{W}) \to x \cdot_{W} y \in {Base}_{W}$
31	18	adantr	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in {Base}_{W} \land z \in {Base}_{W})) \to W \in Ring$
32		simpr1	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \in (S \cap {Base}_{W})$
33	32	elin2d	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \in {Base}_{W}$
34		simpr2	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in {Base}_{W} \land z \in {Base}_{W})) \to y \in {Base}_{W}$
35		simpr3	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in {Base}_{W} \land z \in {Base}_{W})) \to z \in {Base}_{W}$
36	3 11 13	ringdi	$⊢ (W \in Ring \land (x \in {Base}_{W} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \cdot_{W} (y +_{W} z) = (x \cdot_{W} y) +_{W} (x \cdot_{W} z)$
37	31 33 34 35 36	syl13anc	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in {Base}_{W} \land z \in {Base}_{W})) \to x \cdot_{W} (y +_{W} z) = (x \cdot_{W} y) +_{W} (x \cdot_{W} z)$
38	18	adantr	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to W \in Ring$
39		simpr1	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to x \in (S \cap {Base}_{W})$
40	39	elin2d	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to x \in {Base}_{W}$
41		simpr2	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to y \in (S \cap {Base}_{W})$
42	41	elin2d	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to y \in {Base}_{W}$
43		simpr3	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to z \in {Base}_{W}$
44	3 11 13	ringdir	$⊢ (W \in Ring \land (x \in {Base}_{W} \land y \in {Base}_{W} \land z \in {Base}_{W})) \to (x +_{W} y) \cdot_{W} z = (x \cdot_{W} z) +_{W} (y \cdot_{W} z)$
45	38 40 42 43 44	syl13anc	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to (x +_{W} y) \cdot_{W} z = (x \cdot_{W} z) +_{W} (y \cdot_{W} z)$
46	3 13	ringass	$⊢ (W \in Ring \land (x \in {Base}_{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)$
47	38 40 42 43 46	syl13anc	$⊢ (S \in SubRing (W) \land (x \in (S \cap {Base}_{W}) \land y \in (S \cap {Base}_{W}) \land z \in {Base}_{W})) \to (x \cdot_{W} y) \cdot_{W} z = x \cdot_{W} (y \cdot_{W} z)$
48	3 13 15	ringlidm	$⊢ (W \in Ring \land x \in {Base}_{W}) \to 1_{W} \cdot_{W} x = x$
49	18 48	sylan	$⊢ (S \in SubRing (W) \land x \in {Base}_{W}) \to 1_{W} \cdot_{W} x = x$
50	5 6 7 8 10 12 14 16 17 24 30 37 45 47 49	islmodd	$⊢ S \in SubRing (W) \to A \in LMod$

Metamath Proof Explorer

Theorem sralmod

Proof