This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sraassaOLD

Description: Obsolete version of sraassa as of 21-Mar-2025. (Contributed by Mario Carneiro, 6-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sraassa.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
Assertion sraassaOLD ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 sraassa.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
2 1 a1i ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 3 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
5 4 adantl ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
6 2 5 srabase ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
7 2 5 srasca ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑊 ↾s 𝑆 ) = ( Scalar ‘ 𝐴 ) )
8 eqid ⊢ ( 𝑊 ↾s 𝑆 ) = ( 𝑊 ↾s 𝑆 )
9 8 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 = ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) )
10 9 adantl ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 = ( Base ‘ ( 𝑊 ↾s 𝑆 ) ) )
11 2 5 sravsca ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
12 2 5 sramulr ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
13 1 sralmod ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ∈ LMod )
14 13 adantl ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ LMod )
15 crngring ⊢ ( 𝑊 ∈ CRing → 𝑊 ∈ Ring )
16 15 adantr ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑊 ∈ Ring )
17 eqidd ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
18 2 5 sraaddg ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐴 ) )
19 18 oveqdr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
20 12 oveqdr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
21 17 6 19 20 ringpropd ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑊 ∈ Ring ↔ 𝐴 ∈ Ring ) )
22 16 21 mpbid ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ Ring )
23 16 adantr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
24 5 adantr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
25 simpr1 ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ 𝑆 )
26 24 25 sseldd ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
27 simpr2 ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
28 simpr3 ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
29 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
30 3 29 ringass ⊢ ( ( 𝑊 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
31 23 26 27 28 30 syl13anc ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
32 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
33 32 crngmgp ⊢ ( 𝑊 ∈ CRing → ( mulGrp ‘ 𝑊 ) ∈ CMnd )
34 33 ad2antrr ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( mulGrp ‘ 𝑊 ) ∈ CMnd )
35 32 3 mgpbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
36 32 29 mgpplusg ⊢ ( .r ‘ 𝑊 ) = ( +g ‘ ( mulGrp ‘ 𝑊 ) )
37 35 36 cmn12 ⊢ ( ( ( mulGrp ‘ 𝑊 ) ∈ CMnd ∧ ( 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
38 34 27 26 28 37 syl13anc ⊢ ( ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
39 6 7 10 11 12 14 22 31 38 isassad ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )