dsmmlss

Description: The finite hull of a product of modules is additionally closed under scalar multiplication and thus is a linear subspace of the product. (Contributed by Stefan O'Rear, 11-Jan-2015)

	Ref	Expression
Hypotheses	dsmmlss.i	$⊢ φ \to I \in W$
	dsmmlss.s	$⊢ φ \to S \in Ring$
	dsmmlss.r	$⊢ φ \to R : I ⟶ LMod$
	dsmmlss.k	$⊢ (φ \land x \in I) \to Scalar (R (x)) = S$
	dsmmlss.p	$⊢ P = S ⨉_{𝑠} R$
	dsmmlss.u	$⊢ U = LSubSp (P)$
	dsmmlss.h	$⊢ H = {Base}_{(S \oplus_{m} R)}$
Assertion	dsmmlss	$⊢ φ \to H \in U$

Proof

Step	Hyp	Ref	Expression
1		dsmmlss.i	$⊢ φ \to I \in W$
2		dsmmlss.s	$⊢ φ \to S \in Ring$
3		dsmmlss.r	$⊢ φ \to R : I ⟶ LMod$
4		dsmmlss.k	$⊢ (φ \land x \in I) \to Scalar (R (x)) = S$
5		dsmmlss.p	$⊢ P = S ⨉_{𝑠} R$
6		dsmmlss.u	$⊢ U = LSubSp (P)$
7		dsmmlss.h	$⊢ H = {Base}_{(S \oplus_{m} R)}$
8		lmodgrp	$⊢ a \in LMod \to a \in Grp$
9	8	ssriv	$⊢ LMod \subseteq Grp$
10		fss	$⊢ (R : I ⟶ LMod \land LMod \subseteq Grp) \to R : I ⟶ Grp$
11	3 9 10	sylancl	$⊢ φ \to R : I ⟶ Grp$
12	5 7 1 2 11	dsmmsubg	$⊢ φ \to H \in SubGrp (P)$
13	5 2 1 3 4	prdslmodd	$⊢ φ \to P \in LMod$
14	13	adantr	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to P \in LMod$
15		simprl	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to a \in {Base}_{Scalar (P)}$
16		simprr	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to b \in H$
17		eqid	$⊢ S \oplus_{m} R = S \oplus_{m} R$
18		eqid	$⊢ {Base}_{P} = {Base}_{P}$
19	3	ffnd	$⊢ φ \to R Fn I$
20	5 17 18 7 1 19	dsmmelbas	$⊢ φ \to (b \in H \leftrightarrow (b \in {Base}_{P} \land \{x \in I \| b (x) \neq 0_{R (x)}\} \in Fin))$
21	20	adantr	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to (b \in H \leftrightarrow (b \in {Base}_{P} \land \{x \in I \| b (x) \neq 0_{R (x)}\} \in Fin))$
22	16 21	mpbid	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to (b \in {Base}_{P} \land \{x \in I \| b (x) \neq 0_{R (x)}\} \in Fin)$
23	22	simpld	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to b \in {Base}_{P}$
24		eqid	$⊢ Scalar (P) = Scalar (P)$
25		eqid	$⊢ \cdot_{P} = \cdot_{P}$
26		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
27	18 24 25 26	lmodvscl	$⊢ (P \in LMod \land a \in {Base}_{Scalar (P)} \land b \in {Base}_{P}) \to a \cdot_{P} b \in {Base}_{P}$
28	14 15 23 27	syl3anc	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to a \cdot_{P} b \in {Base}_{P}$
29	22	simprd	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to \{x \in I \| b (x) \neq 0_{R (x)}\} \in Fin$
30		eqid	$⊢ {Base}_{S} = {Base}_{S}$
31	2	ad2antrr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to S \in Ring$
32	1	ad2antrr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to I \in W$
33	19	ad2antrr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to R Fn I$
34		fex	$⊢ (R : I ⟶ LMod \land I \in W) \to R \in V$
35	3 1 34	syl2anc	$⊢ φ \to R \in V$
36	5 2 35	prdssca	$⊢ φ \to S = Scalar (P)$
37	36	fveq2d	$⊢ φ \to {Base}_{S} = {Base}_{Scalar (P)}$
38	37	eleq2d	$⊢ φ \to (a \in {Base}_{S} \leftrightarrow a \in {Base}_{Scalar (P)})$
39	38	biimpar	$⊢ (φ \land a \in {Base}_{Scalar (P)}) \to a \in {Base}_{S}$
40	39	adantrr	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to a \in {Base}_{S}$
41	40	adantr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \in {Base}_{S}$
42	23	adantr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to b \in {Base}_{P}$
43		simpr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to x \in I$
44	5 18 25 30 31 32 33 41 42 43	prdsvscafval	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to (a \cdot_{P} b) (x) = a \cdot_{R (x)} b (x)$
45	44	adantrr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land (x \in I \land b (x) = 0_{R (x)})) \to (a \cdot_{P} b) (x) = a \cdot_{R (x)} b (x)$
46	3	ffvelrnda	$⊢ (φ \land x \in I) \to R (x) \in LMod$
47	46	adantlr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to R (x) \in LMod$
48		simplrl	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \in {Base}_{Scalar (P)}$
49	36	adantr	$⊢ (φ \land x \in I) \to S = Scalar (P)$
50	4 49	eqtrd	$⊢ (φ \land x \in I) \to Scalar (R (x)) = Scalar (P)$
51	50	fveq2d	$⊢ (φ \land x \in I) \to {Base}_{Scalar (R (x))} = {Base}_{Scalar (P)}$
52	51	adantlr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to {Base}_{Scalar (R (x))} = {Base}_{Scalar (P)}$
53	48 52	eleqtrrd	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \in {Base}_{Scalar (R (x))}$
54		eqid	$⊢ Scalar (R (x)) = Scalar (R (x))$
55		eqid	$⊢ \cdot_{R (x)} = \cdot_{R (x)}$
56		eqid	$⊢ {Base}_{Scalar (R (x))} = {Base}_{Scalar (R (x))}$
57		eqid	$⊢ 0_{R (x)} = 0_{R (x)}$
58	54 55 56 57	lmodvs0	$⊢ (R (x) \in LMod \land a \in {Base}_{Scalar (R (x))}) \to a \cdot_{R (x)} 0_{R (x)} = 0_{R (x)}$
59	47 53 58	syl2anc	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \cdot_{R (x)} 0_{R (x)} = 0_{R (x)}$
60		oveq2	$⊢ b (x) = 0_{R (x)} \to a \cdot_{R (x)} b (x) = a \cdot_{R (x)} 0_{R (x)}$
61	60	eqeq1d	$⊢ b (x) = 0_{R (x)} \to (a \cdot_{R (x)} b (x) = 0_{R (x)} \leftrightarrow a \cdot_{R (x)} 0_{R (x)} = 0_{R (x)})$
62	59 61	syl5ibrcom	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to (b (x) = 0_{R (x)} \to a \cdot_{R (x)} b (x) = 0_{R (x)})$
63	62	impr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land (x \in I \land b (x) = 0_{R (x)})) \to a \cdot_{R (x)} b (x) = 0_{R (x)}$
64	45 63	eqtrd	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land (x \in I \land b (x) = 0_{R (x)})) \to (a \cdot_{P} b) (x) = 0_{R (x)}$
65	64	expr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to (b (x) = 0_{R (x)} \to (a \cdot_{P} b) (x) = 0_{R (x)})$
66	65	necon3d	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to ((a \cdot_{P} b) (x) \neq 0_{R (x)} \to b (x) \neq 0_{R (x)})$
67	66	ss2rabdv	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to \{x \in I \| (a \cdot_{P} b) (x) \neq 0_{R (x)}\} \subseteq \{x \in I \| b (x) \neq 0_{R (x)}\}$
68	29 67	ssfid	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to \{x \in I \| (a \cdot_{P} b) (x) \neq 0_{R (x)}\} \in Fin$
69	5 17 18 7 1 19	dsmmelbas	$⊢ φ \to (a \cdot_{P} b \in H \leftrightarrow (a \cdot_{P} b \in {Base}_{P} \land \{x \in I \| (a \cdot_{P} b) (x) \neq 0_{R (x)}\} \in Fin))$
70	69	adantr	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to (a \cdot_{P} b \in H \leftrightarrow (a \cdot_{P} b \in {Base}_{P} \land \{x \in I \| (a \cdot_{P} b) (x) \neq 0_{R (x)}\} \in Fin))$
71	28 68 70	mpbir2and	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to a \cdot_{P} b \in H$
72	71	ralrimivva	$⊢ φ \to \forall a \in {Base}_{Scalar (P)} \forall b \in H a \cdot_{P} b \in H$
73	24 26 18 25 6	islss4	$⊢ P \in LMod \to (H \in U \leftrightarrow (H \in SubGrp (P) \land \forall a \in {Base}_{Scalar (P)} \forall b \in H a \cdot_{P} b \in H))$
74	13 73	syl	$⊢ φ \to (H \in U \leftrightarrow (H \in SubGrp (P) \land \forall a \in {Base}_{Scalar (P)} \forall b \in H a \cdot_{P} b \in H))$
75	12 72 74	mpbir2and	$⊢ φ \to H \in U$

Metamath Proof Explorer

Theorem dsmmlss

Proof