Theorem sralmod

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

	Ref	Expression
Hypothesis	sralmod.a	⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
Assertion	sralmod	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		sralmod.a	⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
2	1	a1i	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
3		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4	3	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
5	2 4	srabase	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
6	2 4	sraaddg	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐴 ) )
7	2 4	srasca	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
8	2 4	sravsca	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
9		eqid	⊢ ( 𝑊 ↾s 𝑆 ) = ( 𝑊 ↾s 𝑆 )
10	9 3	ressbas	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) = ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) )
11		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
12	9 11	ressplusg	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( +g ‘ 𝑊 ) = ( +g ‘ ( 𝑊 ↾s 𝑆 ) ) )
13		eqid	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
14	9 13	ressmulr	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( .r ‘ 𝑊 ) = ( .r ‘ ( 𝑊 ↾s 𝑆 ) ) )
15		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
16	9 15	subrg1	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 1r ‘ 𝑊 ) = ( 1r ‘ ( 𝑊 ↾s 𝑆 ) ) )
17	9	subrgring	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 𝑊 ↾s 𝑆 ) ∈ Ring )
18		subrgrcl	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑊 ∈ Ring )
19		ringgrp	⊢ ( 𝑊 ∈ Ring → 𝑊 ∈ Grp )
20	18 19	syl	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑊 ∈ Grp )
21		eqidd	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
22	6	oveqdr	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
23	21 5 22	grppropd	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 𝑊 ∈ Grp ↔ 𝐴 ∈ Grp ) )
24	20 23	mpbid	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ∈ Grp )
25	18	3ad2ant1	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ Ring )
26		elinel2	⊢ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
27	26	3ad2ant2	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
28		simp3	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
29	3 13	ringcl	⊢ ( ( 𝑊 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
30	25 27 28 29	syl3anc	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
31	18	adantr	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
32		simpr1	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) )
33	32	elin2d	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
34		simpr2	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
35		simpr3	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
36	3 11 13	ringdi	⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) )
37	31 33 34 35 36	syl13anc	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) )
38	18	adantr	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
39		simpr1	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) )
40	39	elin2d	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
41		simpr2	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) )
42	41	elin2d	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
43		simpr3	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
44	3 11 13	ringdir	⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ( +g ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
45	38 40 42 43 44	syl13anc	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ( +g ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
46	3 13	ringass	⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
47	38 40 42 43 46	syl13anc	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑆 ∩ ( Base ‘ 𝑊 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
48	3 13 15	ringlidm	⊢ ( ( 𝑊 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑥 ) = 𝑥 )
49	18 48	sylan	⊢ ( ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝑊 ) ( .r ‘ 𝑊 ) 𝑥 ) = 𝑥 )
50	5 6 7 8 10 12 14 16 17 24 30 37 45 47 49	islmodd	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ∈ LMod )