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	3 1	fexd	$⊢ φ \to R \in V$
35	5 2 34	prdssca	$⊢ φ \to S = Scalar (P)$
36	35	fveq2d	$⊢ φ \to {Base}_{S} = {Base}_{Scalar (P)}$
37	36	eleq2d	$⊢ φ \to (a \in {Base}_{S} \leftrightarrow a \in {Base}_{Scalar (P)})$
38	37	biimpar	$⊢ (φ \land a \in {Base}_{Scalar (P)}) \to a \in {Base}_{S}$
39	38	adantrr	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to a \in {Base}_{S}$
40	39	adantr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \in {Base}_{S}$
41	23	adantr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to b \in {Base}_{P}$
42		simpr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to x \in I$
43	5 18 25 30 31 32 33 40 41 42	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)$
44	43	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)$
45	3	ffvelcdmda	$⊢ (φ \land x \in I) \to R (x) \in LMod$
46	45	adantlr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to R (x) \in LMod$
47		simplrl	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \in {Base}_{Scalar (P)}$
48	35	adantr	$⊢ (φ \land x \in I) \to S = Scalar (P)$
49	4 48	eqtrd	$⊢ (φ \land x \in I) \to Scalar (R (x)) = Scalar (P)$
50	49	fveq2d	$⊢ (φ \land x \in I) \to {Base}_{Scalar (R (x))} = {Base}_{Scalar (P)}$
51	50	adantlr	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to {Base}_{Scalar (R (x))} = {Base}_{Scalar (P)}$
52	47 51	eleqtrrd	$⊢ ((φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \land x \in I) \to a \in {Base}_{Scalar (R (x))}$
53		eqid	$⊢ Scalar (R (x)) = Scalar (R (x))$
54		eqid	$⊢ \cdot_{R (x)} = \cdot_{R (x)}$
55		eqid	$⊢ {Base}_{Scalar (R (x))} = {Base}_{Scalar (R (x))}$
56		eqid	$⊢ 0_{R (x)} = 0_{R (x)}$
57	53 54 55 56	lmodvs0	$⊢ (R (x) \in LMod \land a \in {Base}_{Scalar (R (x))}) \to a \cdot_{R (x)} 0_{R (x)} = 0_{R (x)}$
58	46 52 57	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)}$
59		oveq2	$⊢ b (x) = 0_{R (x)} \to a \cdot_{R (x)} b (x) = a \cdot_{R (x)} 0_{R (x)}$
60	59	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)})$
61	58 60	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)})$
62	61	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)}$
63	44 62	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)}$
64	63	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)})$
65	64	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)})$
66	65	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)}\}$
67	29 66	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$
68	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))$
69	68	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))$
70	28 67 69	mpbir2and	$⊢ (φ \land (a \in {Base}_{Scalar (P)} \land b \in H)) \to a \cdot_{P} b \in H$
71	70	ralrimivva	$⊢ φ \to \forall a \in {Base}_{Scalar (P)} \forall b \in H a \cdot_{P} b \in H$
72	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))$
73	13 72	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))$
74	12 71 73	mpbir2and	$⊢ φ \to H \in U$

Metamath Proof Explorer

Theorem dsmmlss

Proof