bj-finsumval0

Description: Value of a finite sum. (Contributed by BJ, 9-Jun-2019) (Proof shortened by AV, 5-May-2021)

	Ref	Expression
Hypotheses	bj-finsumval0.1	$⊢ φ \to A \in CMnd$
	bj-finsumval0.2	$⊢ φ \to I \in Fin$
	bj-finsumval0.3	$⊢ φ \to B : I ⟶ {Base}_{A}$
Assertion	bj-finsumval0	$⊢ φ \to A FinSum B = (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$

Proof

Step	Hyp	Ref	Expression
1		bj-finsumval0.1	$⊢ φ \to A \in CMnd$
2		bj-finsumval0.2	$⊢ φ \to I \in Fin$
3		bj-finsumval0.3	$⊢ φ \to B : I ⟶ {Base}_{A}$
4		df-ov	$⊢ A FinSum B = FinSum (⟨A, B⟩)$
5		df-bj-finsum	$⊢ FinSum = (x \in \{⟨y, z⟩ \| (y \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{y})\} ⟼ (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m))))$
6		simpr	$⊢ (φ \land x = ⟨A, B⟩) \to x = ⟨A, B⟩$
7	6	fveq2d	$⊢ (φ \land x = ⟨A, B⟩) \to 1^{st} (x) = 1^{st} (⟨A, B⟩)$
8	1	adantr	$⊢ (φ \land x = ⟨A, B⟩) \to A \in CMnd$
9	3 2	fexd	$⊢ φ \to B \in V$
10	9	adantr	$⊢ (φ \land x = ⟨A, B⟩) \to B \in V$
11		op1stg	$⊢ (A \in CMnd \land B \in V) \to 1^{st} (⟨A, B⟩) = A$
12	8 10 11	syl2anc	$⊢ (φ \land x = ⟨A, B⟩) \to 1^{st} (⟨A, B⟩) = A$
13	7 12	eqtrd	$⊢ (φ \land x = ⟨A, B⟩) \to 1^{st} (x) = A$
14	6	fveq2d	$⊢ (φ \land x = ⟨A, B⟩) \to 2^{nd} (x) = 2^{nd} (⟨A, B⟩)$
15		op2ndg	$⊢ (A \in CMnd \land B \in V) \to 2^{nd} (⟨A, B⟩) = B$
16	8 10 15	syl2anc	$⊢ (φ \land x = ⟨A, B⟩) \to 2^{nd} (⟨A, B⟩) = B$
17	14 16	eqtrd	$⊢ (φ \land x = ⟨A, B⟩) \to 2^{nd} (x) = B$
18	17	dmeqd	$⊢ (φ \land x = ⟨A, B⟩) \to dom 2^{nd} (x) = dom B$
19	3	fdmd	$⊢ φ \to dom B = I$
20	19	adantr	$⊢ (φ \land x = ⟨A, B⟩) \to dom B = I$
21	18 20	eqtrd	$⊢ (φ \land x = ⟨A, B⟩) \to dom 2^{nd} (x) = I$
22		f1oeq3	$⊢ dom 2^{nd} (x) = I \to (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} I)$
23	22	biimpd	$⊢ dom 2^{nd} (x) = I \to (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \to f : (1 \dots m) \underset{1-1 onto}{⟶} I)$
24	23	ad2antll	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \to f : (1 \dots m) \underset{1-1 onto}{⟶} I)$
25	24	adantrd	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \to f : (1 \dots m) \underset{1-1 onto}{⟶} I)$
26	25	adantr	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \to f : (1 \dots m) \underset{1-1 onto}{⟶} I)$
27		eqidd	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to 1 = 1$
28		simprl	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \to 1^{st} (x) = A$
29	28	fveq2d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \to +_{1^{st} (x)} = +_{A}$
30	29	adantrr	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to +_{1^{st} (x)} = +_{A}$
31		simprrl	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \to 2^{nd} (x) = B$
32	31	adantr	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \land n \in ℕ) \to 2^{nd} (x) = B$
33	32	fveq1d	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \land n \in ℕ) \to 2^{nd} (x) (f (n)) = B (f (n))$
34	33	mpteq2dva	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \to (n \in ℕ ⟼ 2^{nd} (x) (f (n))) = (n \in ℕ ⟼ B (f (n)))$
35	34	adantrr	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (n \in ℕ ⟼ 2^{nd} (x) (f (n))) = (n \in ℕ ⟼ B (f (n)))$
36	27 30 35	seqeq123d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n))))$
37		simprr	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to dom 2^{nd} (x) = I$
38	37	anim1ci	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to (m \in ℕ_{0} \land dom 2^{nd} (x) = I)$
39		hashfz1	$⊢ m \in ℕ_{0} \to \|(1 \dots m)\| = m$
40	39	eqcomd	$⊢ m \in ℕ_{0} \to m = \|(1 \dots m)\|$
41	40	ad2antrl	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to m = \|(1 \dots m)\|$
42		fzfid	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to (1 \dots m) \in Fin$
43		19.8a	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \to \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x)$
44	43	adantr	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to \exists f f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x)$
45		hasheqf1oi	$⊢ (1 \dots m) \in Fin \to (\exists f f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \to \|(1 \dots m)\| = \|dom 2^{nd} (x)\|)$
46	42 44 45	sylc	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to \|(1 \dots m)\| = \|dom 2^{nd} (x)\|$
47		simprr	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to dom 2^{nd} (x) = I$
48	47	fveq2d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to \|dom 2^{nd} (x)\| = \|I\|$
49	41 46 48	3eqtrd	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land (m \in ℕ_{0} \land dom 2^{nd} (x) = I)) \to m = \|I\|$
50	38 49	sylan2	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to m = \|I\|$
51	36 50	fveq12d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m) = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)$
52	51	eqeq2d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m) \leftrightarrow s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))$
53	52	biimpd	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m) \to s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))$
54	53	impancom	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \to (((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))$
55	54	com12	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \to s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))$
56	26 55	jcad	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \to (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
57	22	biimprd	$⊢ dom 2^{nd} (x) = I \to (f : (1 \dots m) \underset{1-1 onto}{⟶} I \to f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x))$
58	57	ad2antll	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to (f : (1 \dots m) \underset{1-1 onto}{⟶} I \to f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x))$
59	58	adantr	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to (f : (1 \dots m) \underset{1-1 onto}{⟶} I \to f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x))$
60	59	adantrd	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)) \to f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x))$
61		eqidd	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to 1 = 1$
62		simpl	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to 1^{st} (x) = A$
63		tru	$⊢ ⊤$
64	62 63	jctir	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to (1^{st} (x) = A \land ⊤)$
65	64	ad2antrl	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (1^{st} (x) = A \land ⊤)$
66		simpl	$⊢ (1^{st} (x) = A \land ⊤) \to 1^{st} (x) = A$
67	66	eqcomd	$⊢ (1^{st} (x) = A \land ⊤) \to A = 1^{st} (x)$
68	65 67	syl	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to A = 1^{st} (x)$
69	68	fveq2d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to +_{A} = +_{1^{st} (x)}$
70		simpl	$⊢ (2^{nd} (x) = B \land dom 2^{nd} (x) = I) \to 2^{nd} (x) = B$
71	70	eqcomd	$⊢ (2^{nd} (x) = B \land dom 2^{nd} (x) = I) \to B = 2^{nd} (x)$
72	71	ad2antll	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \to B = 2^{nd} (x)$
73	72	adantr	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} I \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \land n \in ℕ) \to B = 2^{nd} (x)$
74	73	fveq1d	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} I \land (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I))) \land n \in ℕ) \to B (f (n)) = 2^{nd} (x) (f (n))$
75	74	adantlrr	$⊢ ((f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \land n \in ℕ) \to B (f (n)) = 2^{nd} (x) (f (n))$
76	75	mpteq2dva	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (n \in ℕ ⟼ B (f (n))) = (n \in ℕ ⟼ 2^{nd} (x) (f (n)))$
77	61 69 76	seqeq123d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n))))$
78	59	impcom	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x)$
79		simprr	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to m \in ℕ_{0}$
80	37	ad2antrl	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to dom 2^{nd} (x) = I$
81	78 79 80 49	syl12anc	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to m = \|I\|$
82	81	eqcomd	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to \|I\| = m$
83	77 82	fveq12d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|) = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)$
84	83	eqeq2d	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|) \leftrightarrow s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m))$
85	84	biimpd	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0})) \to (s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|) \to s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m))$
86	85	impancom	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)) \to (((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m))$
87	86	com12	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)) \to s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m))$
88	60 87	jcad	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)) \to (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)))$
89	56 88	impbid	$⊢ ((1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
90	89	ex	$⊢ (1^{st} (x) = A \land (2^{nd} (x) = B \land dom 2^{nd} (x) = I)) \to (m \in ℕ_{0} \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))))$
91	13 17 21 90	syl12anc	$⊢ (φ \land x = ⟨A, B⟩) \to (m \in ℕ_{0} \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))))$
92	91	imp	$⊢ ((φ \land x = ⟨A, B⟩) \land m \in ℕ_{0}) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
93	92	exbidv	$⊢ ((φ \land x = ⟨A, B⟩) \land m \in ℕ_{0}) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
94	93	rexbidva	$⊢ (φ \land x = ⟨A, B⟩) \to (\exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m)) \leftrightarrow \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
95	94	iotabidv	$⊢ (φ \land x = ⟨A, B⟩) \to (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} dom 2^{nd} (x) \land s = seq 1 (+_{1^{st} (x)}, (n \in ℕ ⟼ 2^{nd} (x) (f (n)))) (m))) = (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
96		eleq1	$⊢ t = I \to (t \in Fin \leftrightarrow I \in Fin)$
97		feq2	$⊢ t = I \to (B : t ⟶ {Base}_{A} \leftrightarrow B : I ⟶ {Base}_{A})$
98	96 97	anbi12d	$⊢ t = I \to ((t \in Fin \land B : t ⟶ {Base}_{A}) \leftrightarrow (I \in Fin \land B : I ⟶ {Base}_{A}))$
99	98	ceqsexgv	$⊢ I \in Fin \to (\exists t (t = I \land (t \in Fin \land B : t ⟶ {Base}_{A})) \leftrightarrow (I \in Fin \land B : I ⟶ {Base}_{A}))$
100	2 99	syl	$⊢ φ \to (\exists t (t = I \land (t \in Fin \land B : t ⟶ {Base}_{A})) \leftrightarrow (I \in Fin \land B : I ⟶ {Base}_{A}))$
101	2 3 100	mpbir2and	$⊢ φ \to \exists t (t = I \land (t \in Fin \land B : t ⟶ {Base}_{A}))$
102		exsimpr	$⊢ \exists t (t = I \land (t \in Fin \land B : t ⟶ {Base}_{A})) \to \exists t (t \in Fin \land B : t ⟶ {Base}_{A})$
103	101 102	syl	$⊢ φ \to \exists t (t \in Fin \land B : t ⟶ {Base}_{A})$
104		df-rex	$⊢ \exists t \in Fin B : t ⟶ {Base}_{A} \leftrightarrow \exists t (t \in Fin \land B : t ⟶ {Base}_{A})$
105	103 104	sylibr	$⊢ φ \to \exists t \in Fin B : t ⟶ {Base}_{A}$
106		eleq1	$⊢ y = A \to (y \in CMnd \leftrightarrow A \in CMnd)$
107		fveq2	$⊢ y = A \to {Base}_{y} = {Base}_{A}$
108	107	feq3d	$⊢ y = A \to (z : t ⟶ {Base}_{y} \leftrightarrow z : t ⟶ {Base}_{A})$
109	108	rexbidv	$⊢ y = A \to (\exists t \in Fin z : t ⟶ {Base}_{y} \leftrightarrow \exists t \in Fin z : t ⟶ {Base}_{A})$
110	106 109	anbi12d	$⊢ y = A \to ((y \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{y}) \leftrightarrow (A \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{A}))$
111		feq1	$⊢ z = B \to (z : t ⟶ {Base}_{A} \leftrightarrow B : t ⟶ {Base}_{A})$
112	111	rexbidv	$⊢ z = B \to (\exists t \in Fin z : t ⟶ {Base}_{A} \leftrightarrow \exists t \in Fin B : t ⟶ {Base}_{A})$
113	112	anbi2d	$⊢ z = B \to ((A \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{A}) \leftrightarrow (A \in CMnd \land \exists t \in Fin B : t ⟶ {Base}_{A}))$
114	110 113	opelopabg	$⊢ (A \in CMnd \land B \in V) \to (⟨A, B⟩ \in \{⟨y, z⟩ \| (y \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{y})\} \leftrightarrow (A \in CMnd \land \exists t \in Fin B : t ⟶ {Base}_{A}))$
115	1 9 114	syl2anc	$⊢ φ \to (⟨A, B⟩ \in \{⟨y, z⟩ \| (y \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{y})\} \leftrightarrow (A \in CMnd \land \exists t \in Fin B : t ⟶ {Base}_{A}))$
116	1 105 115	mpbir2and	$⊢ φ \to ⟨A, B⟩ \in \{⟨y, z⟩ \| (y \in CMnd \land \exists t \in Fin z : t ⟶ {Base}_{y})\}$
117		iotaex	$⊢ (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))) \in V$
118	117	a1i	$⊢ φ \to (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|))) \in V$
119	5 95 116 118	fvmptd2	$⊢ φ \to FinSum (⟨A, B⟩) = (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$
120	4 119	syl5eq	$⊢ φ \to A FinSum B = (ι s \| \exists m \in ℕ_{0} \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} I \land s = seq 1 (+_{A}, (n \in ℕ ⟼ B (f (n)))) (\|I\|)))$

Metamath Proof Explorer

Theorem bj-finsumval0

Proof