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 )