ixpsnbasval

Description: The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018)

		Ref	Expression
	Assertion	ixpsnbasval	$⊢ (R \in V \land X \in W) \to \underset{x \in \{X\}}{⨉} {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = \{f \| (f Fn \{X\} \land f (X) \in {Base}_{R})\}$

Proof

Step	Hyp	Ref	Expression
1		ixpsnval	$⊢ X \in W \to \underset{x \in \{X\}}{⨉} {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = \{f \| (f Fn \{X\} \land f (X) \in ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)})\}$
2	1	adantl	$⊢ (R \in V \land X \in W) \to \underset{x \in \{X\}}{⨉} {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = \{f \| (f Fn \{X\} \land f (X) \in ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)})\}$
3		csbfv2g	$⊢ X \in W \to ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = {Base}_{⦋ X / x ⦌ (\{X\} \times \{ringLMod (R)\}) (x)}$
4		csbfv2g	$⊢ X \in W \to ⦋ X / x ⦌ (\{X\} \times \{ringLMod (R)\}) (x) = (\{X\} \times \{ringLMod (R)\}) (⦋ X / x ⦌ x)$
5		csbvarg	$⊢ X \in W \to ⦋ X / x ⦌ x = X$
6	5	fveq2d	$⊢ X \in W \to (\{X\} \times \{ringLMod (R)\}) (⦋ X / x ⦌ x) = (\{X\} \times \{ringLMod (R)\}) (X)$
7	4 6	eqtrd	$⊢ X \in W \to ⦋ X / x ⦌ (\{X\} \times \{ringLMod (R)\}) (x) = (\{X\} \times \{ringLMod (R)\}) (X)$
8	7	fveq2d	$⊢ X \in W \to {Base}_{⦋ X / x ⦌ (\{X\} \times \{ringLMod (R)\}) (x)} = {Base}_{(\{X\} \times \{ringLMod (R)\}) (X)}$
9	3 8	eqtrd	$⊢ X \in W \to ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = {Base}_{(\{X\} \times \{ringLMod (R)\}) (X)}$
10	9	adantl	$⊢ (R \in V \land X \in W) \to ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = {Base}_{(\{X\} \times \{ringLMod (R)\}) (X)}$
11		fvexd	$⊢ R \in V \to ringLMod (R) \in V$
12	11	anim1ci	$⊢ (R \in V \land X \in W) \to (X \in W \land ringLMod (R) \in V)$
13		xpsng	$⊢ (X \in W \land ringLMod (R) \in V) \to \{X\} \times \{ringLMod (R)\} = \{⟨X, ringLMod (R)⟩\}$
14	12 13	syl	$⊢ (R \in V \land X \in W) \to \{X\} \times \{ringLMod (R)\} = \{⟨X, ringLMod (R)⟩\}$
15	14	fveq1d	$⊢ (R \in V \land X \in W) \to (\{X\} \times \{ringLMod (R)\}) (X) = \{⟨X, ringLMod (R)⟩\} (X)$
16		fvsng	$⊢ (X \in W \land ringLMod (R) \in V) \to \{⟨X, ringLMod (R)⟩\} (X) = ringLMod (R)$
17	12 16	syl	$⊢ (R \in V \land X \in W) \to \{⟨X, ringLMod (R)⟩\} (X) = ringLMod (R)$
18	15 17	eqtrd	$⊢ (R \in V \land X \in W) \to (\{X\} \times \{ringLMod (R)\}) (X) = ringLMod (R)$
19	18	fveq2d	$⊢ (R \in V \land X \in W) \to {Base}_{(\{X\} \times \{ringLMod (R)\}) (X)} = {Base}_{ringLMod (R)}$
20	10 19	eqtrd	$⊢ (R \in V \land X \in W) \to ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = {Base}_{ringLMod (R)}$
21		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
22	20 21	eqtr4di	$⊢ (R \in V \land X \in W) \to ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = {Base}_{R}$
23	22	eleq2d	$⊢ (R \in V \land X \in W) \to (f (X) \in ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} \leftrightarrow f (X) \in {Base}_{R})$
24	23	anbi2d	$⊢ (R \in V \land X \in W) \to ((f Fn \{X\} \land f (X) \in ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)}) \leftrightarrow (f Fn \{X\} \land f (X) \in {Base}_{R}))$
25	24	abbidv	$⊢ (R \in V \land X \in W) \to \{f \| (f Fn \{X\} \land f (X) \in ⦋ X / x ⦌ {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)})\} = \{f \| (f Fn \{X\} \land f (X) \in {Base}_{R})\}$
26	2 25	eqtrd	$⊢ (R \in V \land X \in W) \to \underset{x \in \{X\}}{⨉} {Base}_{(\{X\} \times \{ringLMod (R)\}) (x)} = \{f \| (f Fn \{X\} \land f (X) \in {Base}_{R})\}$

Metamath Proof Explorer

Theorem ixpsnbasval

Proof