Theorem issubassa3

Description: A subring that is also a subspace is a subalgebra. The key theorem is islss3 . (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	issubassa.s	⊢ 𝑆 = ( 𝑊 ↾s 𝐴 )
	issubassa.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion	issubassa3	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ AssAlg )

Proof

Step	Hyp	Ref	Expression
1		issubassa.s	⊢ 𝑆 = ( 𝑊 ↾s 𝐴 )
2		issubassa.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3	1	subrgbas	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 = ( Base ‘ 𝑆 ) )
4	3	ad2antrl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
5		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6	1 5	resssca	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑆 ) )
7	6	ad2antrl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑆 ) )
8		eqidd	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
9		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
10	1 9	ressvsca	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑆 ) )
11	10	ad2antrl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑆 ) )
12		eqid	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
13	1 12	ressmulr	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → ( .r ‘ 𝑊 ) = ( .r ‘ 𝑆 ) )
14	13	ad2antrl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( .r ‘ 𝑊 ) = ( .r ‘ 𝑆 ) )
15		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
16		simpr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) → 𝐴 ∈ 𝐿 )
17	1 2	lsslmod	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐿 ) → 𝑆 ∈ LMod )
18	15 16 17	syl2an	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ LMod )
19	1	subrgring	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ∈ Ring )
20	19	ad2antrl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ Ring )
21		idd	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
22		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
23	22	subrgss	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ⊆ ( Base ‘ 𝑊 ) )
24	23	ad2antrl	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝐴 ⊆ ( Base ‘ 𝑊 ) )
25	24	sseld	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( Base ‘ 𝑊 ) ) )
26	24	sseld	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( Base ‘ 𝑊 ) ) )
27	21 25 26	3anim123d	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) )
28	27	imp	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) )
29		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
30	22 5 29 9 12	assaass	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
31	30	adantlr	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
32	28 31	syldan	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
33	22 5 29 9 12	assaassr	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
34	33	adantlr	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
35	28 34	syldan	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
36	4 7 8 11 14 18 20 32 35	isassad	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ AssAlg )