psrplusgpropd

Description: Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015) (Revised by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	psrplusgpropd.b1	$⊢ φ \to B = {Base}_{R}$
	psrplusgpropd.b2	$⊢ φ \to B = {Base}_{S}$
	psrplusgpropd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{S} y$
Assertion	psrplusgpropd	$⊢ φ \to +_{(I mPwSer R)} = +_{(I mPwSer S)}$

Proof

Step	Hyp	Ref	Expression
1		psrplusgpropd.b1	$⊢ φ \to B = {Base}_{R}$
2		psrplusgpropd.b2	$⊢ φ \to B = {Base}_{S}$
3		psrplusgpropd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{R} y = x +_{S} y$
4		simpl1	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to φ$
5		eqid	$⊢ I mPwSer R = I mPwSer R$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} = \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}$
8		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
9		simp2	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to a \in {Base}_{(I mPwSer R)}$
10	5 6 7 8 9	psrelbas	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to a : \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
11	10	ffvelcdmda	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to a (d) \in {Base}_{R}$
12	4 1	syl	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to B = {Base}_{R}$
13	11 12	eleqtrrd	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to a (d) \in B$
14		simp3	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to b \in {Base}_{(I mPwSer R)}$
15	5 6 7 8 14	psrelbas	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to b : \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
16	15	ffvelcdmda	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to b (d) \in {Base}_{R}$
17	16 12	eleqtrrd	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to b (d) \in B$
18	3	oveqrspc2v	$⊢ (φ \land (a (d) \in B \land b (d) \in B)) \to a (d) +_{R} b (d) = a (d) +_{S} b (d)$
19	4 13 17 18	syl12anc	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to a (d) +_{R} b (d) = a (d) +_{S} b (d)$
20	19	mpteq2dva	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to (d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} ⟼ a (d) +_{R} b (d)) = (d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} ⟼ a (d) +_{S} b (d))$
21	10	ffnd	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to a Fn \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}$
22	15	ffnd	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to b Fn \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}$
23		ovex	$⊢ {ℕ_{0}}^{I} \in V$
24	23	rabex	$⊢ \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} \in V$
25	24	a1i	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} \in V$
26		inidm	$⊢ \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} \cap \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} = \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}$
27		eqidd	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to a (d) = a (d)$
28		eqidd	$⊢ ((φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \land d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\}) \to b (d) = b (d)$
29	21 22 25 25 26 27 28	offval	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to a {+_{R}}_{f} b = (d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} ⟼ a (d) +_{R} b (d))$
30	21 22 25 25 26 27 28	offval	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to a {+_{S}}_{f} b = (d \in \{c \in ({ℕ_{0}}^{I}) \| c^{-1} [ℕ] \in Fin\} ⟼ a (d) +_{S} b (d))$
31	20 29 30	3eqtr4d	$⊢ (φ \land a \in {Base}_{(I mPwSer R)} \land b \in {Base}_{(I mPwSer R)}) \to a {+_{R}}_{f} b = a {+_{S}}_{f} b$
32	31	mpoeq3dva	$⊢ φ \to (a \in {Base}_{(I mPwSer R)}, b \in {Base}_{(I mPwSer R)} ⟼ a {+_{R}}_{f} b) = (a \in {Base}_{(I mPwSer R)}, b \in {Base}_{(I mPwSer R)} ⟼ a {+_{S}}_{f} b)$
33	1 2	eqtr3d	$⊢ φ \to {Base}_{R} = {Base}_{S}$
34	33	psrbaspropd	$⊢ φ \to {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer S)}$
35		mpoeq12	$⊢ ({Base}_{(I mPwSer R)} = {Base}_{(I mPwSer S)} \land {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer S)}) \to (a \in {Base}_{(I mPwSer R)}, b \in {Base}_{(I mPwSer R)} ⟼ a {+_{S}}_{f} b) = (a \in {Base}_{(I mPwSer S)}, b \in {Base}_{(I mPwSer S)} ⟼ a {+_{S}}_{f} b)$
36	34 34 35	syl2anc	$⊢ φ \to (a \in {Base}_{(I mPwSer R)}, b \in {Base}_{(I mPwSer R)} ⟼ a {+_{S}}_{f} b) = (a \in {Base}_{(I mPwSer S)}, b \in {Base}_{(I mPwSer S)} ⟼ a {+_{S}}_{f} b)$
37	32 36	eqtrd	$⊢ φ \to (a \in {Base}_{(I mPwSer R)}, b \in {Base}_{(I mPwSer R)} ⟼ a {+_{R}}_{f} b) = (a \in {Base}_{(I mPwSer S)}, b \in {Base}_{(I mPwSer S)} ⟼ a {+_{S}}_{f} b)$
38		ofmres	$⊢ {\circ_{f} +_{R} ↾}_{({Base}_{(I mPwSer R)} \times {Base}_{(I mPwSer R)})} = (a \in {Base}_{(I mPwSer R)}, b \in {Base}_{(I mPwSer R)} ⟼ a {+_{R}}_{f} b)$
39		ofmres	$⊢ {\circ_{f} +_{S} ↾}_{({Base}_{(I mPwSer S)} \times {Base}_{(I mPwSer S)})} = (a \in {Base}_{(I mPwSer S)}, b \in {Base}_{(I mPwSer S)} ⟼ a {+_{S}}_{f} b)$
40	37 38 39	3eqtr4g	$⊢ φ \to {\circ_{f} +_{R} ↾}_{({Base}_{(I mPwSer R)} \times {Base}_{(I mPwSer R)})} = {\circ_{f} +_{S} ↾}_{({Base}_{(I mPwSer S)} \times {Base}_{(I mPwSer S)})}$
41		eqid	$⊢ +_{R} = +_{R}$
42		eqid	$⊢ +_{(I mPwSer R)} = +_{(I mPwSer R)}$
43	5 8 41 42	psrplusg	$⊢ +_{(I mPwSer R)} = {\circ_{f} +_{R} ↾}_{({Base}_{(I mPwSer R)} \times {Base}_{(I mPwSer R)})}$
44		eqid	$⊢ I mPwSer S = I mPwSer S$
45		eqid	$⊢ {Base}_{(I mPwSer S)} = {Base}_{(I mPwSer S)}$
46		eqid	$⊢ +_{S} = +_{S}$
47		eqid	$⊢ +_{(I mPwSer S)} = +_{(I mPwSer S)}$
48	44 45 46 47	psrplusg	$⊢ +_{(I mPwSer S)} = {\circ_{f} +_{S} ↾}_{({Base}_{(I mPwSer S)} \times {Base}_{(I mPwSer S)})}$
49	40 43 48	3eqtr4g	$⊢ φ \to +_{(I mPwSer R)} = +_{(I mPwSer S)}$

Metamath Proof Explorer

Theorem psrplusgpropd

Proof