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 5 assasca ⊢ ( 𝑊 ∈ AssAlg → ( Scalar ‘ 𝑊 ) ∈ CRing )
22 21 adantr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( Scalar ‘ 𝑊 ) ∈ CRing )
23 idd ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
24 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
25 24 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 ⊆ ( Base ‘ 𝑊 ) )
26 25 ad2antrl ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝐴 ⊆ ( Base ‘ 𝑊 ) )
27 26 sseld ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( Base ‘ 𝑊 ) ) )
28 26 sseld ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( Base ‘ 𝑊 ) ) )
29 23 27 28 3anim123d ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → ( ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) )
30 29 imp ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) )
31 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
32 24 5 31 9 12 assaass ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
33 32 adantlr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
34 30 33 syldan ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( .r ‘ 𝑊 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
35 24 5 31 9 12 assaassr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
36 35 adantlr ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
37 30 36 syldan ⊢ ( ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 ( .r ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( .r ‘ 𝑊 ) 𝑧 ) ) )
38 4 7 8 11 14 18 20 22 34 37 isassad ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐿 ) ) → 𝑆 ∈ AssAlg )