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 = {Base}_{W}$
	islss3.s	$⊢ S = LSubSp (W)$
Assertion	islss3	$⊢ W \in LMod \to (U \in S \leftrightarrow (U \subseteq V \land X \in LMod))$

Proof

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

Metamath Proof Explorer

Theorem islss3

Proof