# 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}=\mathrm{LSubSp}\left({W}\right)$
Assertion issubassa3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in \mathrm{SubRing}\left({W}\right)\wedge {A}\in {L}\right)\right)\to {S}\in \mathrm{AssAlg}$

### Proof

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