Metamath Proof Explorer

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 )