psrass23l

Description: Associative identity for the ring of power series. Part of psrass23 which does not require the scalar ring to be commutative. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	psrring.s	$⊢ S = I mPwSer R$
	psrring.i	$⊢ φ \to I \in V$
	psrring.r	$⊢ φ \to R \in Ring$
	psrass.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrass.t	$⊢ \underset{˙}{\times} = \cdot_{S}$
	psrass.b	$⊢ B = {Base}_{S}$
	psrass.x	$⊢ φ \to X \in B$
	psrass.y	$⊢ φ \to Y \in B$
	psrass23l.k	$⊢ K = {Base}_{R}$
	psrass23l.n	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	psrass23l.a	$⊢ φ \to A \in K$
Assertion	psrass23l	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Proof

Step	Hyp	Ref	Expression
1		psrring.s	$⊢ S = I mPwSer R$
2		psrring.i	$⊢ φ \to I \in V$
3		psrring.r	$⊢ φ \to R \in Ring$
4		psrass.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		psrass.t	$⊢ \underset{˙}{\times} = \cdot_{S}$
6		psrass.b	$⊢ B = {Base}_{S}$
7		psrass.x	$⊢ φ \to X \in B$
8		psrass.y	$⊢ φ \to Y \in B$
9		psrass23l.k	$⊢ K = {Base}_{R}$
10		psrass23l.n	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
11		psrass23l.a	$⊢ φ \to A \in K$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	11	adantr	$⊢ (φ \land k \in D) \to A \in K$
15	14 9	eleqtrdi	$⊢ (φ \land k \in D) \to A \in {Base}_{R}$
16	15	adantr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to A \in {Base}_{R}$
17	7	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X \in B$
18		ssrab2	$⊢ \{y \in D \| y \leq_{f} k\} \subseteq D$
19		simpr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in \{y \in D \| y \leq_{f} k\}$
20	18 19	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
21	1 10 12 6 13 4 16 17 20	psrvscaval	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (A \underset{˙}{\cdot} X) (x) = A \cdot_{R} X (x)$
22	21	oveq1d	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x) = (A \cdot_{R} X (x)) \cdot_{R} Y (k -_{f} x)$
23	3	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
24	1 12 4 6 17	psrelbas	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
25	24 20	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
26	8	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y \in B$
27	1 12 4 6 26	psrelbas	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
28	2	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to I \in V$
29		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
30		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
31	4 30	psrbagconcl	$⊢ (I \in V \land k \in D \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in D \| y \leq_{f} k\}$
32	28 29 19 31	syl3anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in D \| y \leq_{f} k\}$
33	18 32	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
34	27 33	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
35	12 13	ringass	$⊢ (R \in Ring \land (A \in {Base}_{R} \land X (x) \in {Base}_{R} \land Y (k -_{f} x) \in {Base}_{R})) \to (A \cdot_{R} X (x)) \cdot_{R} Y (k -_{f} x) = A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x))$
36	23 16 25 34 35	syl13anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (A \cdot_{R} X (x)) \cdot_{R} Y (k -_{f} x) = A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x))$
37	22 36	eqtrd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x) = A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x))$
38	37	mpteq2dva	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ (A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x)))$
39	38	oveq2d	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} ((A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x)) = \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x)))$
40		eqid	$⊢ 0_{R} = 0_{R}$
41		eqid	$⊢ +_{R} = +_{R}$
42	3	adantr	$⊢ (φ \land k \in D) \to R \in Ring$
43	4	psrbaglefi	$⊢ (I \in V \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
44	2 43	sylan	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
45	12 13	ringcl	$⊢ (R \in Ring \land X (x) \in {Base}_{R} \land Y (k -_{f} x) \in {Base}_{R}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
46	23 25 34 45	syl3anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
47		ovex	$⊢ {ℕ_{0}}^{I} \in V$
48	4 47	rabex2	$⊢ D \in V$
49	48	mptrabex	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \in V$
50		funmpt	$⊢ Fun (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x))$
51		fvex	$⊢ 0_{R} \in V$
52	49 50 51	3pm3.2i	$⊢ ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \in V \land Fun (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \land 0_{R} \in V)$
53	52	a1i	$⊢ (φ \land k \in D) \to ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \in V \land Fun (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \land 0_{R} \in V)$
54		suppssdm	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) supp 0_{R} \subseteq dom (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x))$
55		eqid	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x))$
56	55	dmmptss	$⊢ dom (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \subseteq \{y \in D \| y \leq_{f} k\}$
57	54 56	sstri	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) supp 0_{R} \subseteq \{y \in D \| y \leq_{f} k\}$
58	57	a1i	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) supp 0_{R} \subseteq \{y \in D \| y \leq_{f} k\}$
59		suppssfifsupp	$⊢ (((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \in V \land Fun (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \land 0_{R} \in V) \land (\{y \in D \| y \leq_{f} k\} \in Fin \land (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) supp 0_{R} \subseteq \{y \in D \| y \leq_{f} k\})) \to {finSupp}_{0_{R}} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)))$
60	53 44 58 59	syl12anc	$⊢ (φ \land k \in D) \to {finSupp}_{0_{R}} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)))$
61	12 40 41 13 42 44 15 46 60	gsummulc2	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x))) = A \cdot_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x)))$
62	39 61	eqtrd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} ((A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x)) = A \cdot_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x)))$
63	62	mpteq2dva	$⊢ φ \to (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} ((A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x))) = (k \in D ⟼ A \cdot_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))))$
64	1 10 9 6 3 11 7	psrvscacl	$⊢ φ \to A \underset{˙}{\cdot} X \in B$
65	1 6 13 5 4 64 8	psrmulfval	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} ((A \underset{˙}{\cdot} X) (x) \cdot_{R} Y (k -_{f} x)))$
66	1 6 5 3 7 8	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Y \in B$
67	1 10 9 6 13 4 11 66	psrvsca	$⊢ φ \to A \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (D \times \{A\}) {\cdot_{R}}_{f} (X \underset{˙}{\times} Y)$
68	48	a1i	$⊢ φ \to D \in V$
69		ovexd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) \in V$
70		fconstmpt	$⊢ D \times \{A\} = (k \in D ⟼ A)$
71	70	a1i	$⊢ φ \to D \times \{A\} = (k \in D ⟼ A)$
72	1 6 13 5 4 7 8	psrmulfval	$⊢ φ \to X \underset{˙}{\times} Y = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)))$
73	68 14 69 71 72	offval2	$⊢ φ \to (D \times \{A\}) {\cdot_{R}}_{f} (X \underset{˙}{\times} Y) = (k \in D ⟼ A \cdot_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))))$
74	67 73	eqtrd	$⊢ φ \to A \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (k \in D ⟼ A \cdot_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))))$
75	63 65 74	3eqtr4d	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem psrass23l

Proof