# Metamath Proof Explorer

## Theorem islss3

Description: A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses islss3.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
islss3.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
islss3.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion islss3 ${⊢}{W}\in \mathrm{LMod}\to \left({U}\in {S}↔\left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)$

### Proof

Step Hyp Ref Expression
1 islss3.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
2 islss3.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
3 islss3.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
4 2 3 lssss ${⊢}{U}\in {S}\to {U}\subseteq {V}$
5 4 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\subseteq {V}$
6 1 2 ressbas2 ${⊢}{U}\subseteq {V}\to {U}={\mathrm{Base}}_{{X}}$
7 6 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\subseteq {V}\right)\to {U}={\mathrm{Base}}_{{X}}$
8 4 7 sylan2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}={\mathrm{Base}}_{{X}}$
9 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
10 1 9 ressplusg ${⊢}{U}\in {S}\to {+}_{{W}}={+}_{{X}}$
11 10 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {+}_{{W}}={+}_{{X}}$
12 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
13 1 12 resssca ${⊢}{U}\in {S}\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({X}\right)$
14 13 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({X}\right)$
15 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
16 1 15 ressvsca ${⊢}{U}\in {S}\to {\cdot }_{{W}}={\cdot }_{{X}}$
17 16 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {\cdot }_{{W}}={\cdot }_{{X}}$
18 eqidd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
19 eqidd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
20 eqidd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
21 eqidd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {1}_{\mathrm{Scalar}\left({W}\right)}={1}_{\mathrm{Scalar}\left({W}\right)}$
22 12 lmodring ${⊢}{W}\in \mathrm{LMod}\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}$
23 22 adantr ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}$
24 3 lsssubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
25 1 subggrp ${⊢}{U}\in \mathrm{SubGrp}\left({W}\right)\to {X}\in \mathrm{Grp}$
26 24 25 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {X}\in \mathrm{Grp}$
27 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
28 12 15 27 3 lssvscl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\right)\right)\to {x}{\cdot }_{{W}}{a}\in {U}$
29 28 3impb ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\right)\to {x}{\cdot }_{{W}}{a}\in {U}$
30 simpll ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {W}\in \mathrm{LMod}$
31 simpr1 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
32 4 ad2antlr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {U}\subseteq {V}$
33 simpr2 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {a}\in {U}$
34 32 33 sseldd ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {a}\in {V}$
35 simpr3 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {b}\in {U}$
36 32 35 sseldd ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {b}\in {V}$
37 2 9 12 15 27 lmodvsdi ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {V}\wedge {b}\in {V}\right)\right)\to {x}{\cdot }_{{W}}\left({a}{+}_{{W}}{b}\right)=\left({x}{\cdot }_{{W}}{a}\right){+}_{{W}}\left({x}{\cdot }_{{W}}{b}\right)$
38 30 31 34 36 37 syl13anc ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {U}\wedge {b}\in {U}\right)\right)\to {x}{\cdot }_{{W}}\left({a}{+}_{{W}}{b}\right)=\left({x}{\cdot }_{{W}}{a}\right){+}_{{W}}\left({x}{\cdot }_{{W}}{b}\right)$
39 simpll ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to {W}\in \mathrm{LMod}$
40 simpr1 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
41 simpr2 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
42 4 ad2antlr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to {U}\subseteq {V}$
43 simpr3 ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to {b}\in {U}$
44 42 43 sseldd ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to {b}\in {V}$
45 eqid ${⊢}{+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
46 2 9 12 15 27 45 lmodvsdir ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {V}\right)\right)\to \left({x}{+}_{\mathrm{Scalar}\left({W}\right)}{a}\right){\cdot }_{{W}}{b}=\left({x}{\cdot }_{{W}}{b}\right){+}_{{W}}\left({a}{\cdot }_{{W}}{b}\right)$
47 39 40 41 44 46 syl13anc ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to \left({x}{+}_{\mathrm{Scalar}\left({W}\right)}{a}\right){\cdot }_{{W}}{b}=\left({x}{\cdot }_{{W}}{b}\right){+}_{{W}}\left({a}{\cdot }_{{W}}{b}\right)$
48 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
49 2 12 15 27 48 lmodvsass ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {V}\right)\right)\to \left({x}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{a}\right){\cdot }_{{W}}{b}={x}{\cdot }_{{W}}\left({a}{\cdot }_{{W}}{b}\right)$
50 39 40 41 44 49 syl13anc ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {a}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {b}\in {U}\right)\right)\to \left({x}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{a}\right){\cdot }_{{W}}{b}={x}{\cdot }_{{W}}\left({a}{\cdot }_{{W}}{b}\right)$
51 5 sselda ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\to {x}\in {V}$
52 eqid ${⊢}{1}_{\mathrm{Scalar}\left({W}\right)}={1}_{\mathrm{Scalar}\left({W}\right)}$
53 2 12 15 52 lmodvs1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {x}\in {V}\right)\to {1}_{\mathrm{Scalar}\left({W}\right)}{\cdot }_{{W}}{x}={x}$
54 53 adantlr ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {V}\right)\to {1}_{\mathrm{Scalar}\left({W}\right)}{\cdot }_{{W}}{x}={x}$
55 51 54 syldan ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\to {1}_{\mathrm{Scalar}\left({W}\right)}{\cdot }_{{W}}{x}={x}$
56 8 11 14 17 18 19 20 21 23 26 29 38 47 50 55 islmodd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {X}\in \mathrm{LMod}$
57 5 56 jca ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)$
58 simprl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {U}\subseteq {V}$
59 58 6 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {U}={\mathrm{Base}}_{{X}}$
60 fvex ${⊢}{\mathrm{Base}}_{{X}}\in \mathrm{V}$
61 59 60 eqeltrdi ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {U}\in \mathrm{V}$
62 1 12 resssca ${⊢}{U}\in \mathrm{V}\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({X}\right)$
63 61 62 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({X}\right)$
64 63 eqcomd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to \mathrm{Scalar}\left({X}\right)=\mathrm{Scalar}\left({W}\right)$
65 eqidd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
66 2 a1i ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {V}={\mathrm{Base}}_{{W}}$
67 1 9 ressplusg ${⊢}{U}\in \mathrm{V}\to {+}_{{W}}={+}_{{X}}$
68 61 67 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {+}_{{W}}={+}_{{X}}$
69 68 eqcomd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {+}_{{X}}={+}_{{W}}$
70 1 15 ressvsca ${⊢}{U}\in \mathrm{V}\to {\cdot }_{{W}}={\cdot }_{{X}}$
71 61 70 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\cdot }_{{W}}={\cdot }_{{X}}$
72 71 eqcomd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\cdot }_{{X}}={\cdot }_{{W}}$
73 3 a1i ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {S}=\mathrm{LSubSp}\left({W}\right)$
74 59 58 eqsstrrd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\mathrm{Base}}_{{X}}\subseteq {V}$
75 lmodgrp ${⊢}{X}\in \mathrm{LMod}\to {X}\in \mathrm{Grp}$
76 75 ad2antll ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {X}\in \mathrm{Grp}$
77 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
78 77 grpbn0 ${⊢}{X}\in \mathrm{Grp}\to {\mathrm{Base}}_{{X}}\ne \varnothing$
79 76 78 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\mathrm{Base}}_{{X}}\ne \varnothing$
80 eqid ${⊢}\mathrm{LSubSp}\left({X}\right)=\mathrm{LSubSp}\left({X}\right)$
81 77 80 lss1 ${⊢}{X}\in \mathrm{LMod}\to {\mathrm{Base}}_{{X}}\in \mathrm{LSubSp}\left({X}\right)$
82 81 ad2antll ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\mathrm{Base}}_{{X}}\in \mathrm{LSubSp}\left({X}\right)$
83 eqid ${⊢}\mathrm{Scalar}\left({X}\right)=\mathrm{Scalar}\left({X}\right)$
84 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
85 eqid ${⊢}{+}_{{X}}={+}_{{X}}$
86 eqid ${⊢}{\cdot }_{{X}}={\cdot }_{{X}}$
87 83 84 85 86 80 lsscl ${⊢}\left({\mathrm{Base}}_{{X}}\in \mathrm{LSubSp}\left({X}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge {a}\in {\mathrm{Base}}_{{X}}\wedge {b}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left({x}{\cdot }_{{X}}{a}\right){+}_{{X}}{b}\in {\mathrm{Base}}_{{X}}$
88 82 87 sylan ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}\wedge {a}\in {\mathrm{Base}}_{{X}}\wedge {b}\in {\mathrm{Base}}_{{X}}\right)\right)\to \left({x}{\cdot }_{{X}}{a}\right){+}_{{X}}{b}\in {\mathrm{Base}}_{{X}}$
89 64 65 66 69 72 73 74 79 88 islssd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {\mathrm{Base}}_{{X}}\in {S}$
90 59 89 eqeltrd ${⊢}\left({W}\in \mathrm{LMod}\wedge \left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)\to {U}\in {S}$
91 57 90 impbida ${⊢}{W}\in \mathrm{LMod}\to \left({U}\in {S}↔\left({U}\subseteq {V}\wedge {X}\in \mathrm{LMod}\right)\right)$