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 = W ↾ 𝑠 A
issubassa.l ⊢ L = LSubSp ⁡ W
Assertion issubassa3 ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → S ∈ AssAlg

Proof

Step Hyp Ref Expression
1 issubassa.s ⊢ S = W ↾ 𝑠 A
2 issubassa.l ⊢ L = LSubSp ⁡ W
3 1 subrgbas ⊢ A ∈ SubRing ⁡ W → A = Base S
4 3 ad2antrl ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → A = Base S
5 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
6 1 5 resssca ⊢ A ∈ SubRing ⁡ W → Scalar ⁡ W = Scalar ⁡ S
7 6 ad2antrl ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → Scalar ⁡ W = Scalar ⁡ S
8 eqidd ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → Base Scalar ⁡ W = Base Scalar ⁡ W
9 eqid ⊢ ⋅ W = ⋅ W
10 1 9 ressvsca ⊢ A ∈ SubRing ⁡ W → ⋅ W = ⋅ S
11 10 ad2antrl ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → ⋅ W = ⋅ S
12 eqid ⊢ ⋅ W = ⋅ W
13 1 12 ressmulr ⊢ A ∈ SubRing ⁡ W → ⋅ W = ⋅ S
14 13 ad2antrl ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → ⋅ W = ⋅ S
15 assalmod ⊢ W ∈ AssAlg → W ∈ LMod
16 simpr ⊢ A ∈ SubRing ⁡ W ∧ A ∈ L → A ∈ L
17 1 2 lsslmod ⊢ W ∈ LMod ∧ A ∈ L → S ∈ LMod
18 15 16 17 syl2an ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → S ∈ LMod
19 1 subrgring ⊢ A ∈ SubRing ⁡ W → S ∈ Ring
20 19 ad2antrl ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → S ∈ Ring
21 5 assasca ⊢ W ∈ AssAlg → Scalar ⁡ W ∈ CRing
22 21 adantr ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → Scalar ⁡ W ∈ CRing
23 idd ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → x ∈ Base Scalar ⁡ W → x ∈ Base Scalar ⁡ W
24 eqid ⊢ Base W = Base W
25 24 subrgss ⊢ A ∈ SubRing ⁡ W → A ⊆ Base W
26 25 ad2antrl ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → A ⊆ Base W
27 26 sseld ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → y ∈ A → y ∈ Base W
28 26 sseld ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → z ∈ A → z ∈ Base W
29 23 27 28 3anim123d ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → x ∈ Base Scalar ⁡ W ∧ y ∈ A ∧ z ∈ A → x ∈ Base Scalar ⁡ W ∧ y ∈ Base W ∧ z ∈ Base W
30 29 imp ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ A ∧ z ∈ A → x ∈ Base Scalar ⁡ W ∧ y ∈ Base W ∧ z ∈ Base W
31 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
32 24 5 31 9 12 assaass ⊢ W ∈ AssAlg ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ Base W ∧ z ∈ Base W → x ⋅ W y ⋅ W z = x ⋅ W y ⋅ W z
33 32 adantlr ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ Base W ∧ z ∈ Base W → x ⋅ W y ⋅ W z = x ⋅ W y ⋅ W z
34 30 33 syldan ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ A ∧ z ∈ A → x ⋅ W y ⋅ W z = x ⋅ W y ⋅ W z
35 24 5 31 9 12 assaassr ⊢ W ∈ AssAlg ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ Base W ∧ z ∈ Base W → y ⋅ W x ⋅ W z = x ⋅ W y ⋅ W z
36 35 adantlr ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ Base W ∧ z ∈ Base W → y ⋅ W x ⋅ W z = x ⋅ W y ⋅ W z
37 30 36 syldan ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L ∧ x ∈ Base Scalar ⁡ W ∧ y ∈ A ∧ z ∈ A → y ⋅ W x ⋅ W z = x ⋅ W y ⋅ W z
38 4 7 8 11 14 18 20 22 34 37 isassad ⊢ W ∈ AssAlg ∧ A ∈ SubRing ⁡ W ∧ A ∈ L → S ∈ AssAlg