psrass23

Description: Associative identities for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 25-Nov-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$
	psrcom.c	$⊢ φ \to R \in CRing$
	psrass.k	$⊢ K = {Base}_{R}$
	psrass.n	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	psrass.a	$⊢ φ \to A \in K$
Assertion	psrass23	$⊢ φ \to ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \land X \underset{˙}{\times} (A \underset{˙}{\cdot} 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		psrcom.c	$⊢ φ \to R \in CRing$
10		psrass.k	$⊢ K = {Base}_{R}$
11		psrass.n	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
12		psrass.a	$⊢ φ \to A \in K$
13	1 2 3 4 5 6 7 8 10 11 12	psrass23l	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16	12	adantr	$⊢ (φ \land k \in D) \to A \in K$
17	16 10	eleqtrdi	$⊢ (φ \land k \in D) \to A \in {Base}_{R}$
18	17	adantr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to A \in {Base}_{R}$
19	8	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y \in B$
20		ssrab2	$⊢ \{y \in D \| y \leq_{f} k\} \subseteq D$
21		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
22		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\}$
23		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
24	4 23	psrbagconcl	$⊢ (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\}$
25	21 22 24	syl2anc	$⊢ ((φ \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\}$
26	20 25	sselid	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
27	1 11 14 6 15 4 18 19 26	psrvscaval	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (A \underset{˙}{\cdot} Y) (k -_{f} x) = A \cdot_{R} Y (k -_{f} x)$
28	27	oveq2d	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} (A \underset{˙}{\cdot} Y) (k -_{f} x) = X (x) \cdot_{R} (A \cdot_{R} Y (k -_{f} x))$
29	7	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X \in B$
30	1 14 4 6 29	psrelbas	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
31	20 22	sselid	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
32	30 31	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
33	1 14 4 6 19	psrelbas	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
34	33 26	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
35	9	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in CRing$
36	14 15	crngcom	$⊢ (R \in CRing \land u \in {Base}_{R} \land v \in {Base}_{R}) \to u \cdot_{R} v = v \cdot_{R} u$
37	36	3expb	$⊢ (R \in CRing \land (u \in {Base}_{R} \land v \in {Base}_{R})) \to u \cdot_{R} v = v \cdot_{R} u$
38	35 37	sylan	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land (u \in {Base}_{R} \land v \in {Base}_{R})) \to u \cdot_{R} v = v \cdot_{R} u$
39	3	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
40	14 15	ringass	$⊢ (R \in Ring \land (u \in {Base}_{R} \land v \in {Base}_{R} \land w \in {Base}_{R})) \to (u \cdot_{R} v) \cdot_{R} w = u \cdot_{R} (v \cdot_{R} w)$
41	39 40	sylan	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land (u \in {Base}_{R} \land v \in {Base}_{R} \land w \in {Base}_{R})) \to (u \cdot_{R} v) \cdot_{R} w = u \cdot_{R} (v \cdot_{R} w)$
42	32 18 34 38 41	caov12d	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} (A \cdot_{R} Y (k -_{f} x)) = A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x))$
43	28 42	eqtrd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} (A \underset{˙}{\cdot} Y) (k -_{f} x) = A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x))$
44	43	mpteq2dva	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} (A \underset{˙}{\cdot} Y) (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ A \cdot_{R} (X (x) \cdot_{R} Y (k -_{f} x)))$
45	44	oveq2d	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (A \underset{˙}{\cdot} 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)))$
46		eqid	$⊢ 0_{R} = 0_{R}$
47		eqid	$⊢ +_{R} = +_{R}$
48	3	adantr	$⊢ (φ \land k \in D) \to R \in Ring$
49	4	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
50	49	adantl	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
51	14 15	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}$
52	39 32 34 51	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}$
53		ovex	$⊢ {ℕ_{0}}^{I} \in V$
54	4 53	rabex2	$⊢ D \in V$
55	54	mptrabex	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) \in V$
56		funmpt	$⊢ Fun (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x))$
57		fvex	$⊢ 0_{R} \in V$
58	55 56 57	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)$
59	58	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)$
60		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))$
61		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))$
62	61	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\}$
63	60 62	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\}$
64	63	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\}$
65		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)))$
66	59 50 64 65	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)))$
67	14 46 47 15 48 50 17 52 66	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)))$
68	45 67	eqtrd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (A \underset{˙}{\cdot} 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)))$
69	68	mpteq2dva	$⊢ φ \to (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (A \underset{˙}{\cdot} 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))))$
70	1 11 10 6 3 12 8	psrvscacl	$⊢ φ \to A \underset{˙}{\cdot} Y \in B$
71	1 6 15 5 4 7 70	psrmulfval	$⊢ φ \to X \underset{˙}{\times} (A \underset{˙}{\cdot} Y) = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (A \underset{˙}{\cdot} Y) (k -_{f} x)))$
72	1 6 5 3 7 8	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Y \in B$
73	1 11 10 6 15 4 12 72	psrvsca	$⊢ φ \to A \underset{˙}{\cdot} (X \underset{˙}{\times} Y) = (D \times \{A\}) {\cdot_{R}}_{f} (X \underset{˙}{\times} Y)$
74	54	a1i	$⊢ φ \to D \in V$
75		ovex	$⊢ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) \in V$
76	75	a1i	$⊢ (φ \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$
77		fconstmpt	$⊢ D \times \{A\} = (k \in D ⟼ A)$
78	77	a1i	$⊢ φ \to D \times \{A\} = (k \in D ⟼ A)$
79	1 6 15 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)))$
80	74 16 76 78 79	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))))$
81	73 80	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))))$
82	69 71 81	3eqtr4d	$⊢ φ \to X \underset{˙}{\times} (A \underset{˙}{\cdot} Y) = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$
83	13 82	jca	$⊢ φ \to ((A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y) \land X \underset{˙}{\times} (A \underset{˙}{\cdot} Y) = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y))$

Metamath Proof Explorer

Theorem psrass23

Proof