frlmbas

Description: Base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

	Ref	Expression
Hypotheses	frlmval.f	$⊢ F = R freeLMod I$
	frlmbas.n	$⊢ N = {Base}_{R}$
	frlmbas.z	$⊢ \underset{˙}{0} = 0_{R}$
	frlmbas.b	$⊢ B = \{k \in (N^{I}) \| {finSupp}_{\underset{˙}{0}} (k)\}$
Assertion	frlmbas	$⊢ (R \in V \land I \in W) \to B = {Base}_{F}$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$⊢ F = R freeLMod I$
2		frlmbas.n	$⊢ N = {Base}_{R}$
3		frlmbas.z	$⊢ \underset{˙}{0} = 0_{R}$
4		frlmbas.b	$⊢ B = \{k \in (N^{I}) \| {finSupp}_{\underset{˙}{0}} (k)\}$
5		fvex	$⊢ ringLMod (R) \in V$
6		fnconstg	$⊢ ringLMod (R) \in V \to (I \times \{ringLMod (R)\}) Fn I$
7	5 6	ax-mp	$⊢ (I \times \{ringLMod (R)\}) Fn I$
8		eqid	$⊢ R ⨉_{𝑠} (I \times \{ringLMod (R)\}) = R ⨉_{𝑠} (I \times \{ringLMod (R)\})$
9		eqid	$⊢ \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\} = \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\}$
10	8 9	dsmmbas2	$⊢ ((I \times \{ringLMod (R)\}) Fn I \land I \in W) \to \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\} = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
11	7 10	mpan	$⊢ I \in W \to \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\} = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
12	11	adantl	$⊢ (R \in V \land I \in W) \to \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\} = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
13		fvco2	$⊢ ((I \times \{ringLMod (R)\}) Fn I \land x \in I) \to (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x) = 0_{(I \times \{ringLMod (R)\}) (x)}$
14	7 13	mpan	$⊢ x \in I \to (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x) = 0_{(I \times \{ringLMod (R)\}) (x)}$
15	14	adantl	$⊢ (((R \in V \land I \in W) \land k \in (N^{I})) \land x \in I) \to (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x) = 0_{(I \times \{ringLMod (R)\}) (x)}$
16	5	fvconst2	$⊢ x \in I \to (I \times \{ringLMod (R)\}) (x) = ringLMod (R)$
17	16	adantl	$⊢ (((R \in V \land I \in W) \land k \in (N^{I})) \land x \in I) \to (I \times \{ringLMod (R)\}) (x) = ringLMod (R)$
18	17	fveq2d	$⊢ (((R \in V \land I \in W) \land k \in (N^{I})) \land x \in I) \to 0_{(I \times \{ringLMod (R)\}) (x)} = 0_{ringLMod (R)}$
19		rlm0	$⊢ 0_{R} = 0_{ringLMod (R)}$
20	3 19	eqtri	$⊢ \underset{˙}{0} = 0_{ringLMod (R)}$
21	18 20	eqtr4di	$⊢ (((R \in V \land I \in W) \land k \in (N^{I})) \land x \in I) \to 0_{(I \times \{ringLMod (R)\}) (x)} = \underset{˙}{0}$
22	15 21	eqtrd	$⊢ (((R \in V \land I \in W) \land k \in (N^{I})) \land x \in I) \to (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x) = \underset{˙}{0}$
23	22	neeq2d	$⊢ (((R \in V \land I \in W) \land k \in (N^{I})) \land x \in I) \to (k (x) \neq (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x) \leftrightarrow k (x) \neq \underset{˙}{0})$
24	23	rabbidva	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to \{x \in I \| k (x) \neq (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x)\} = \{x \in I \| k (x) \neq \underset{˙}{0}\}$
25		elmapfn	$⊢ k \in (N^{I}) \to k Fn I$
26	25	adantl	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to k Fn I$
27		fn0g	$⊢ 0_{𝑔} Fn V$
28		ssv	$⊢ ran (I \times \{ringLMod (R)\}) \subseteq V$
29		fnco	$⊢ (0_{𝑔} Fn V \land (I \times \{ringLMod (R)\}) Fn I \land ran (I \times \{ringLMod (R)\}) \subseteq V) \to (0_{𝑔} \circ (I \times \{ringLMod (R)\})) Fn I$
30	27 7 28 29	mp3an	$⊢ (0_{𝑔} \circ (I \times \{ringLMod (R)\})) Fn I$
31		fndmdif	$⊢ (k Fn I \land (0_{𝑔} \circ (I \times \{ringLMod (R)\})) Fn I) \to dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) = \{x \in I \| k (x) \neq (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x)\}$
32	26 30 31	sylancl	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) = \{x \in I \| k (x) \neq (0_{𝑔} \circ (I \times \{ringLMod (R)\})) (x)\}$
33		simplr	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to I \in W$
34	3	fvexi	$⊢ \underset{˙}{0} \in V$
35	34	a1i	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to \underset{˙}{0} \in V$
36		suppvalfn	$⊢ (k Fn I \land I \in W \land \underset{˙}{0} \in V) \to k supp \underset{˙}{0} = \{x \in I \| k (x) \neq \underset{˙}{0}\}$
37	26 33 35 36	syl3anc	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to k supp \underset{˙}{0} = \{x \in I \| k (x) \neq \underset{˙}{0}\}$
38	24 32 37	3eqtr4d	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) = k supp \underset{˙}{0}$
39	38	eleq1d	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to (dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin \leftrightarrow k supp \underset{˙}{0} \in Fin)$
40		elmapfun	$⊢ k \in (N^{I}) \to Fun k$
41		id	$⊢ k \in (N^{I}) \to k \in (N^{I})$
42	34	a1i	$⊢ k \in (N^{I}) \to \underset{˙}{0} \in V$
43	40 41 42	3jca	$⊢ k \in (N^{I}) \to (Fun k \land k \in (N^{I}) \land \underset{˙}{0} \in V)$
44	43	adantl	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to (Fun k \land k \in (N^{I}) \land \underset{˙}{0} \in V)$
45		funisfsupp	$⊢ (Fun k \land k \in (N^{I}) \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (k) \leftrightarrow k supp \underset{˙}{0} \in Fin)$
46	44 45	syl	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to ({finSupp}_{\underset{˙}{0}} (k) \leftrightarrow k supp \underset{˙}{0} \in Fin)$
47	39 46	bitr4d	$⊢ ((R \in V \land I \in W) \land k \in (N^{I})) \to (dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin \leftrightarrow {finSupp}_{\underset{˙}{0}} (k))$
48	47	rabbidva	$⊢ (R \in V \land I \in W) \to \{k \in (N^{I}) \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\} = \{k \in (N^{I}) \| {finSupp}_{\underset{˙}{0}} (k)\}$
49		eqid	$⊢ ringLMod (R) ↑_{𝑠} I = ringLMod (R) ↑_{𝑠} I$
50		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
51	2 50	eqtri	$⊢ N = {Base}_{ringLMod (R)}$
52	49 51	pwsbas	$⊢ (ringLMod (R) \in V \land I \in W) \to N^{I} = {Base}_{(ringLMod (R) ↑_{𝑠} I)}$
53	5 52	mpan	$⊢ I \in W \to N^{I} = {Base}_{(ringLMod (R) ↑_{𝑠} I)}$
54	53	adantl	$⊢ (R \in V \land I \in W) \to N^{I} = {Base}_{(ringLMod (R) ↑_{𝑠} I)}$
55		eqid	$⊢ Scalar (ringLMod (R)) = Scalar (ringLMod (R))$
56	49 55	pwsval	$⊢ (ringLMod (R) \in V \land I \in W) \to ringLMod (R) ↑_{𝑠} I = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
57	5 56	mpan	$⊢ I \in W \to ringLMod (R) ↑_{𝑠} I = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
58	57	adantl	$⊢ (R \in V \land I \in W) \to ringLMod (R) ↑_{𝑠} I = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
59		rlmsca	$⊢ R \in V \to R = Scalar (ringLMod (R))$
60	59	adantr	$⊢ (R \in V \land I \in W) \to R = Scalar (ringLMod (R))$
61	60	oveq1d	$⊢ (R \in V \land I \in W) \to R ⨉_{𝑠} (I \times \{ringLMod (R)\}) = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
62	58 61	eqtr4d	$⊢ (R \in V \land I \in W) \to ringLMod (R) ↑_{𝑠} I = R ⨉_{𝑠} (I \times \{ringLMod (R)\})$
63	62	fveq2d	$⊢ (R \in V \land I \in W) \to {Base}_{(ringLMod (R) ↑_{𝑠} I)} = {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))}$
64	54 63	eqtrd	$⊢ (R \in V \land I \in W) \to N^{I} = {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))}$
65	64	rabeqdv	$⊢ (R \in V \land I \in W) \to \{k \in (N^{I}) \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\} = \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\}$
66	48 65	eqtr3d	$⊢ (R \in V \land I \in W) \to \{k \in (N^{I}) \| {finSupp}_{\underset{˙}{0}} (k)\} = \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\}$
67	4 66	syl5eq	$⊢ (R \in V \land I \in W) \to B = \{k \in {Base}_{(R ⨉_{𝑠} (I \times \{ringLMod (R)\}))} \| dom (k ∖ (0_{𝑔} \circ (I \times \{ringLMod (R)\}))) \in Fin\}$
68	1	frlmval	$⊢ (R \in V \land I \in W) \to F = R \oplus_{m} (I \times \{ringLMod (R)\})$
69	68	fveq2d	$⊢ (R \in V \land I \in W) \to {Base}_{F} = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
70	12 67 69	3eqtr4d	$⊢ (R \in V \land I \in W) \to B = {Base}_{F}$

Metamath Proof Explorer

Theorem frlmbas

Proof