Metamath Proof Explorer

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 )