jensen

Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015) (Proof shortened by AV, 27-Jul-2019)

	Ref	Expression
Hypotheses	jensen.1	$⊢ φ \to D \subseteq ℝ$
	jensen.2	$⊢ φ \to F : D ⟶ ℝ$
	jensen.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
	jensen.4	$⊢ φ \to A \in Fin$
	jensen.5	$⊢ φ \to T : A ⟶ [0, +∞)$
	jensen.6	$⊢ φ \to X : A ⟶ D$
	jensen.7	$⊢ φ \to 0 < \sum_{ℂ_{fld}} T$
	jensen.8	$⊢ (φ \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
Assertion	jensen	$⊢ φ \to (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in D \land F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$

Proof

Step	Hyp	Ref	Expression
1		jensen.1	$⊢ φ \to D \subseteq ℝ$
2		jensen.2	$⊢ φ \to F : D ⟶ ℝ$
3		jensen.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
4		jensen.4	$⊢ φ \to A \in Fin$
5		jensen.5	$⊢ φ \to T : A ⟶ [0, +∞)$
6		jensen.6	$⊢ φ \to X : A ⟶ D$
7		jensen.7	$⊢ φ \to 0 < \sum_{ℂ_{fld}} T$
8		jensen.8	$⊢ (φ \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
9	5	ffnd	$⊢ φ \to T Fn A$
10		fnresdm	$⊢ T Fn A \to {T ↾}_{A} = T$
11	9 10	syl	$⊢ φ \to {T ↾}_{A} = T$
12	11	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ({T ↾}_{A}) = \sum_{ℂ_{fld}} T$
13	7 12	breqtrrd	$⊢ φ \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})$
14		ssid	$⊢ A \subseteq A$
15	13 14	jctil	$⊢ φ \to (A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A}))$
16		sseq1	$⊢ a = \emptyset \to (a \subseteq A \leftrightarrow \emptyset \subseteq A)$
17		reseq2	$⊢ a = \emptyset \to {T ↾}_{a} = {T ↾}_{\emptyset}$
18		res0	$⊢ {T ↾}_{\emptyset} = \emptyset$
19	17 18	eqtrdi	$⊢ a = \emptyset \to {T ↾}_{a} = \emptyset$
20	19	oveq2d	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} \emptyset$
21		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
22	21	gsum0	$⊢ \sum_{ℂ_{fld}} \emptyset = 0$
23	20 22	eqtrdi	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = 0$
24	23	breq2d	$⊢ a = \emptyset \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < 0)$
25	16 24	anbi12d	$⊢ a = \emptyset \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (\emptyset \subseteq A \land 0 < 0))$
26		reseq2	$⊢ a = \emptyset \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{\emptyset}$
27	26	oveq2d	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})$
28	27 23	oveq12d	$⊢ a = \emptyset \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0}$
29		reseq2	$⊢ a = \emptyset \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{\emptyset}$
30	29	oveq2d	$⊢ a = \emptyset \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})$
31	30 23	oveq12d	$⊢ a = \emptyset \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}$
32	31	breq2d	$⊢ a = \emptyset \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0})$
33	32	rabbidv	$⊢ a = \emptyset \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}$
34	28 33	eleq12d	$⊢ a = \emptyset \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\})$
35	25 34	imbi12d	$⊢ a = \emptyset \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}))$
36	35	imbi2d	$⊢ a = \emptyset \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\})))$
37		sseq1	$⊢ a = k \to (a \subseteq A \leftrightarrow k \subseteq A)$
38		reseq2	$⊢ a = k \to {T ↾}_{a} = {T ↾}_{k}$
39	38	oveq2d	$⊢ a = k \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} ({T ↾}_{k})$
40	39	breq2d	$⊢ a = k \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < \sum_{ℂ_{fld}} ({T ↾}_{k}))$
41	37 40	anbi12d	$⊢ a = k \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})))$
42		reseq2	$⊢ a = k \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{k}$
43	42	oveq2d	$⊢ a = k \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})$
44	43 39	oveq12d	$⊢ a = k \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}$
45		reseq2	$⊢ a = k \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{k}$
46	45	oveq2d	$⊢ a = k \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})$
47	46 39	oveq12d	$⊢ a = k \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}$
48	47	breq2d	$⊢ a = k \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
49	48	rabbidv	$⊢ a = k \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}$
50	44 49	eleq12d	$⊢ a = k \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})$
51	41 50	imbi12d	$⊢ a = k \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}))$
52	51	imbi2d	$⊢ a = k \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})))$
53		sseq1	$⊢ a = k \cup \{c\} \to (a \subseteq A \leftrightarrow k \cup \{c\} \subseteq A)$
54		reseq2	$⊢ a = k \cup \{c\} \to {T ↾}_{a} = {T ↾}_{(k \cup \{c\})}$
55	54	oveq2d	$⊢ a = k \cup \{c\} \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})$
56	55	breq2d	$⊢ a = k \cup \{c\} \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))$
57	53 56	anbi12d	$⊢ a = k \cup \{c\} \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})))$
58		reseq2	$⊢ a = k \cup \{c\} \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{(k \cup \{c\})}$
59	58	oveq2d	$⊢ a = k \cup \{c\} \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})$
60	59 55	oveq12d	$⊢ a = k \cup \{c\} \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}$
61		reseq2	$⊢ a = k \cup \{c\} \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}$
62	61	oveq2d	$⊢ a = k \cup \{c\} \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})$
63	62 55	oveq12d	$⊢ a = k \cup \{c\} \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}$
64	63	breq2d	$⊢ a = k \cup \{c\} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
65	64	rabbidv	$⊢ a = k \cup \{c\} \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}$
66	60 65	eleq12d	$⊢ a = k \cup \{c\} \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
67	57 66	imbi12d	$⊢ a = k \cup \{c\} \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}))$
68	67	imbi2d	$⊢ a = k \cup \{c\} \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
69		sseq1	$⊢ a = A \to (a \subseteq A \leftrightarrow A \subseteq A)$
70		reseq2	$⊢ a = A \to {T ↾}_{a} = {T ↾}_{A}$
71	70	oveq2d	$⊢ a = A \to \sum_{ℂ_{fld}} ({T ↾}_{a}) = \sum_{ℂ_{fld}} ({T ↾}_{A})$
72	71	breq2d	$⊢ a = A \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{a}) \leftrightarrow 0 < \sum_{ℂ_{fld}} ({T ↾}_{A}))$
73	69 72	anbi12d	$⊢ a = A \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \leftrightarrow (A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})))$
74		reseq2	$⊢ a = A \to {(T \times_{f} X) ↾}_{a} = {(T \times_{f} X) ↾}_{A}$
75	74	oveq2d	$⊢ a = A \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})$
76	75 71	oveq12d	$⊢ a = A \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}$
77		reseq2	$⊢ a = A \to {(T \times_{f} (F \circ X)) ↾}_{a} = {(T \times_{f} (F \circ X)) ↾}_{A}$
78	77	oveq2d	$⊢ a = A \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a}) = \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})$
79	78 71	oveq12d	$⊢ a = A \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}$
80	79	breq2d	$⊢ a = A \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})})$
81	80	rabbidv	$⊢ a = A \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}$
82	76 81	eleq12d	$⊢ a = A \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\} \leftrightarrow \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\})$
83	73 82	imbi12d	$⊢ a = A \to (((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\}) \leftrightarrow ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}))$
84	83	imbi2d	$⊢ a = A \to ((φ \to ((a \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{a})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{a})}{\sum_{ℂ_{fld}} ({T ↾}_{a})}\})) \leftrightarrow (φ \to ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\})))$
85		0re	$⊢ 0 \in ℝ$
86	85	ltnri	$⊢ \neg 0 < 0$
87	86	pm2.21i	$⊢ 0 < 0 \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}$
88	87	adantl	$⊢ (\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\}$
89	88	a1i	$⊢ φ \to ((\emptyset \subseteq A \land 0 < 0) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{\emptyset})}{0} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{\emptyset})}{0}\})$
90		impexp	$⊢ ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \leftrightarrow (k \subseteq A \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}))$
91		simprl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \cup \{c\} \subseteq A$
92	91	unssad	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \subseteq A$
93		simpr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})$
94	1	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to D \subseteq ℝ$
95	2	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to F : D ⟶ ℝ$
96		simplll	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to φ$
97	96 3	sylan	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
98	96 4	syl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to A \in Fin$
99	96 5	syl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to T : A ⟶ [0, +∞)$
100	96 6	syl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to X : A ⟶ D$
101	7	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to 0 < \sum_{ℂ_{fld}} T$
102	96 8	sylan	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
103		simpllr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \neg c \in k$
104	91	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to k \cup \{c\} \subseteq A$
105		eqid	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) = \sum_{ℂ_{fld}} ({T ↾}_{k})$
106		eqid	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}) = \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})$
107		cnring	$⊢ ℂ_{fld} \in Ring$
108		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
109	107 108	mp1i	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ℂ_{fld} \in CMnd$
110	4	ad2antrr	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to A \in Fin$
111	110 92	ssfid	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \in Fin$
112		rege0subm	$⊢ [0, +∞) \in SubMnd (ℂ_{fld})$
113	112	a1i	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to [0, +∞) \in SubMnd (ℂ_{fld})$
114	5	ad2antrr	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to T : A ⟶ [0, +∞)$
115	114 92	fssresd	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ({T ↾}_{k}) : k ⟶ [0, +∞)$
116		c0ex	$⊢ 0 \in V$
117	116	a1i	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to 0 \in V$
118	115 111 117	fdmfifsupp	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to {finSupp}_{0} (({T ↾}_{k}))$
119	21 109 111 113 115 118	gsumsubmcl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞)$
120		elrege0	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞) \leftrightarrow (\sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ \land 0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k}))$
121	120	simplbi	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ$
122	119 121	syl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ$
123	122	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ$
124		simprl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})$
125	123 124	elrpd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ^{+}$
126		simprr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}$
127		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \to F (w) = F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
128	127	breq1d	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \leftrightarrow F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
129	128	elrab	$⊢ \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\} \leftrightarrow (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
130	126 129	sylib	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})})$
131	130	simpld	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in D$
132	130	simprd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}$
133	94 95 97 98 99 100 101 102 103 104 105 106 125 131 132	jensenlem2	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
134		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \to F (w) = F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
135	134	breq1d	$⊢ w = \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \leftrightarrow F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
136	135	elrab	$⊢ \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\} \leftrightarrow (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})})$
137	133 136	sylibr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \land \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}$
138	137	expr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\} \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
139	93 138	embantd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ((0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
140		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
141		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
142	107 141	mp1i	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ℂ_{fld} \in Mnd$
143	110 91	ssfid	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to k \cup \{c\} \in Fin$
144	143	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \cup \{c\} \in Fin$
145		ssun2	$⊢ \{c\} \subseteq k \cup \{c\}$
146		vsnid	$⊢ c \in \{c\}$
147	145 146	sselii	$⊢ c \in (k \cup \{c\})$
148	147	a1i	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to c \in (k \cup \{c\})$
149		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
150	149	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
151		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
152		fss	$⊢ (T : A ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to T : A ⟶ ℝ$
153	5 151 152	sylancl	$⊢ φ \to T : A ⟶ ℝ$
154	6 1	fssd	$⊢ φ \to X : A ⟶ ℝ$
155		inidm	$⊢ A \cap A = A$
156	150 153 154 4 4 155	off	$⊢ φ \to (T \times_{f} X) : A ⟶ ℝ$
157		ax-resscn	$⊢ ℝ \subseteq ℂ$
158		fss	$⊢ ((T \times_{f} X) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (T \times_{f} X) : A ⟶ ℂ$
159	156 157 158	sylancl	$⊢ φ \to (T \times_{f} X) : A ⟶ ℂ$
160	159	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} X) : A ⟶ ℂ$
161	91	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \cup \{c\} \subseteq A$
162	160 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
163	5	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T : A ⟶ [0, +∞)$
164	110	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to A \in Fin$
165	163 164	fexd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T \in V$
166	6	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X : A ⟶ D$
167	166 164	fexd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X \in V$
168		offres	$⊢ (T \in V \land X \in V) \to {(T \times_{f} X) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})$
169	165 167 168	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to {(T \times_{f} X) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})$
170	169	oveq1d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) supp 0 = (({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})) supp 0$
171	151 157	sstri	$⊢ [0, +∞) \subseteq ℂ$
172		fss	$⊢ (T : A ⟶ [0, +∞) \land [0, +∞) \subseteq ℂ) \to T : A ⟶ ℂ$
173	163 171 172	sylancl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T : A ⟶ ℂ$
174	173 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({T ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
175		eldifi	$⊢ x \in ((k \cup \{c\}) ∖ \{c\}) \to x \in (k \cup \{c\})$
176	175	adantl	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to x \in (k \cup \{c\})$
177	176	fvresd	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to ({T ↾}_{(k \cup \{c\})}) (x) = T (x)$
178		difun2	$⊢ (k \cup \{c\}) ∖ \{c\} = k ∖ \{c\}$
179		difss	$⊢ k ∖ \{c\} \subseteq k$
180	178 179	eqsstri	$⊢ (k \cup \{c\}) ∖ \{c\} \subseteq k$
181	180	sseli	$⊢ x \in ((k \cup \{c\}) ∖ \{c\}) \to x \in k$
182		simpr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})$
183	92	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \subseteq A$
184	163 183	feqresmpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to {T ↾}_{k} = (x \in k ⟼ T (x))$
185	184	oveq2d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({T ↾}_{k}) = \underset{x \in k}{\sum_{ℂ_{fld}}} T (x)$
186	111	adantr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to k \in Fin$
187	183	sselda	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to x \in A$
188	163	ffvelrnda	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in A) \to T (x) \in [0, +∞)$
189	187 188	syldan	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) \in [0, +∞)$
190	171 189	sselid	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) \in ℂ$
191	186 190	gsumfsum	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \underset{x \in k}{\sum_{ℂ_{fld}}} T (x) = \sum_{x \in k} T (x)$
192	182 185 191	3eqtrrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{x \in k} T (x) = 0$
193		elrege0	$⊢ T (x) \in [0, +∞) \leftrightarrow (T (x) \in ℝ \land 0 \leq T (x))$
194	189 193	sylib	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to (T (x) \in ℝ \land 0 \leq T (x))$
195	194	simpld	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) \in ℝ$
196	194	simprd	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to 0 \leq T (x)$
197	186 195 196	fsum00	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (\sum_{x \in k} T (x) = 0 \leftrightarrow \forall x \in k T (x) = 0)$
198	192 197	mpbid	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \forall x \in k T (x) = 0$
199	198	r19.21bi	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in k) \to T (x) = 0$
200	181 199	sylan2	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to T (x) = 0$
201	177 200	eqtrd	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ((k \cup \{c\}) ∖ \{c\})) \to ({T ↾}_{(k \cup \{c\})}) (x) = 0$
202	174 201	suppss	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({T ↾}_{(k \cup \{c\})}) supp 0 \subseteq \{c\}$
203		mul02	$⊢ x \in ℂ \to 0 \cdot x = 0$
204	203	adantl	$⊢ ((((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \land x \in ℂ) \to 0 \cdot x = 0$
205	1	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to D \subseteq ℝ$
206	205 157	sstrdi	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to D \subseteq ℂ$
207	166 206	fssd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X : A ⟶ ℂ$
208	207 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({X ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
209	116	a1i	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 \in V$
210	202 204 174 208 144 209	suppssof1	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (({T ↾}_{(k \cup \{c\})}) \times_{f} ({X ↾}_{(k \cup \{c\})})) supp 0 \subseteq \{c\}$
211	170 210	eqsstrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) supp 0 \subseteq \{c\}$
212	140 21 142 144 148 162 211	gsumpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) = ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) (c)$
213	148	fvresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) (c) = (T \times_{f} X) (c)$
214	163	ffnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T Fn A$
215	166	ffnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X Fn A$
216	161 148	sseldd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to c \in A$
217		fnfvof	$⊢ ((T Fn A \land X Fn A) \land (A \in Fin \land c \in A)) \to (T \times_{f} X) (c) = T (c) X (c)$
218	214 215 164 216 217	syl22anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} X) (c) = T (c) X (c)$
219	212 213 218	3eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})}) = T (c) X (c)$
220	140 21 142 144 148 174 202	gsumpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}) = ({T ↾}_{(k \cup \{c\})}) (c)$
221	148	fvresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({T ↾}_{(k \cup \{c\})}) (c) = T (c)$
222	220 221	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}) = T (c)$
223	219 222	oveq12d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = \frac{T (c) X (c)}{T (c)}$
224	207 216	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X (c) \in ℂ$
225	173 216	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T (c) \in ℂ$
226		simplrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})$
227	226 222	breqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to 0 < T (c)$
228	227	gt0ne0d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T (c) \neq 0$
229	224 225 228	divcan3d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{T (c) X (c)}{T (c)} = X (c)$
230	223 229	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = X (c)$
231	166 216	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to X (c) \in D$
232	230 231	eqeltrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in D$
233	2	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F : D ⟶ ℝ$
234	233 231	ffvelrnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (X (c)) \in ℝ$
235	234	leidd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (X (c)) \leq F (X (c))$
236	230	fveq2d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) = F (X (c))$
237		fco	$⊢ (F : D ⟶ ℝ \land X : A ⟶ D) \to (F \circ X) : A ⟶ ℝ$
238	2 6 237	syl2anc	$⊢ φ \to (F \circ X) : A ⟶ ℝ$
239	150 153 238 4 4 155	off	$⊢ φ \to (T \times_{f} (F \circ X)) : A ⟶ ℝ$
240		fss	$⊢ ((T \times_{f} (F \circ X)) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (T \times_{f} (F \circ X)) : A ⟶ ℂ$
241	239 157 240	sylancl	$⊢ φ \to (T \times_{f} (F \circ X)) : A ⟶ ℂ$
242	241	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} (F \circ X)) : A ⟶ ℂ$
243	242 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
244	238	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) : A ⟶ ℝ$
245	244 164	fexd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F \circ X \in V$
246		offres	$⊢ (T \in V \land F \circ X \in V) \to {(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})$
247	165 245 246	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to {(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})} = ({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})$
248	247	oveq1d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) supp 0 = (({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})) supp 0$
249		fss	$⊢ ((F \circ X) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (F \circ X) : A ⟶ ℂ$
250	244 157 249	sylancl	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) : A ⟶ ℂ$
251	250 161	fssresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(F \circ X) ↾}_{(k \cup \{c\})}) : k \cup \{c\} ⟶ ℂ$
252	202 204 174 251 144 209	suppssof1	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (({T ↾}_{(k \cup \{c\})}) \times_{f} ({(F \circ X) ↾}_{(k \cup \{c\})})) supp 0 \subseteq \{c\}$
253	248 252	eqsstrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) supp 0 \subseteq \{c\}$
254	140 21 142 144 148 243 253	gsumpt	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) = ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) (c)$
255	148	fvresd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) (c) = (T \times_{f} (F \circ X)) (c)$
256	2	ffnd	$⊢ φ \to F Fn D$
257		fnfco	$⊢ (F Fn D \land X : A ⟶ D) \to (F \circ X) Fn A$
258	256 6 257	syl2anc	$⊢ φ \to (F \circ X) Fn A$
259	258	ad3antrrr	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) Fn A$
260		fnfvof	$⊢ ((T Fn A \land (F \circ X) Fn A) \land (A \in Fin \land c \in A)) \to (T \times_{f} (F \circ X)) (c) = T (c) (F \circ X) (c)$
261	214 259 164 216 260	syl22anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} (F \circ X)) (c) = T (c) (F \circ X) (c)$
262		fvco3	$⊢ (X : A ⟶ D \land c \in A) \to (F \circ X) (c) = F (X (c))$
263	166 216 262	syl2anc	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (F \circ X) (c) = F (X (c))$
264	263	oveq2d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to T (c) (F \circ X) (c) = T (c) F (X (c))$
265	261 264	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to (T \times_{f} (F \circ X)) (c) = T (c) F (X (c))$
266	254 255 265	3eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})}) = T (c) F (X (c))$
267	266 222	oveq12d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = \frac{T (c) F (X (c))}{T (c)}$
268	234	recnd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (X (c)) \in ℂ$
269	268 225 228	divcan3d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{T (c) F (X (c))}{T (c)} = F (X (c))$
270	267 269	eqtrd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} = F (X (c))$
271	235 236 270	3brtr4d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}$
272	135 232 271	elrabd	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}$
273	272	a1d	$⊢ (((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \land 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})) \to ((0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
274	120	simprbi	$⊢ \sum_{ℂ_{fld}} ({T ↾}_{k}) \in [0, +∞) \to 0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k})$
275	119 274	syl	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to 0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k})$
276		leloe	$⊢ (0 \in ℝ \land \sum_{ℂ_{fld}} ({T ↾}_{k}) \in ℝ) \to (0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k}) \leftrightarrow (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \lor 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})))$
277	85 122 276	sylancr	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to (0 \leq \sum_{ℂ_{fld}} ({T ↾}_{k}) \leftrightarrow (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \lor 0 = \sum_{ℂ_{fld}} ({T ↾}_{k})))$
278	275 277	mpbid	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \lor 0 = \sum_{ℂ_{fld}} ({T ↾}_{k}))$
279	139 273 278	mpjaodan	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ((0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
280	92 279	embantd	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to ((k \subseteq A \to (0 < \sum_{ℂ_{fld}} ({T ↾}_{k}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
281	90 280	syl5bi	$⊢ ((φ \land \neg c \in k) \land (k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})}))) \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})$
282	281	ex	$⊢ (φ \land \neg c \in k) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}))$
283	282	com23	$⊢ (φ \land \neg c \in k) \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\}))$
284	283	expcom	$⊢ \neg c \in k \to (φ \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
285	284	adantl	$⊢ (k \in Fin \land \neg c \in k) \to (φ \to (((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\}) \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
286	285	a2d	$⊢ (k \in Fin \land \neg c \in k) \to ((φ \to ((k \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{k})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{k})}{\sum_{ℂ_{fld}} ({T ↾}_{k})}\})) \to (φ \to ((k \cup \{c\} \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(k \cup \{c\})})}{\sum_{ℂ_{fld}} ({T ↾}_{(k \cup \{c\})})}\})))$
287	36 52 68 84 89 286	findcard2s	$⊢ A \in Fin \to (φ \to ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}))$
288	4 287	mpcom	$⊢ φ \to ((A \subseteq A \land 0 < \sum_{ℂ_{fld}} ({T ↾}_{A})) \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\})$
289	15 288	mpd	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\}$
290	156	ffnd	$⊢ φ \to (T \times_{f} X) Fn A$
291		fnresdm	$⊢ (T \times_{f} X) Fn A \to {(T \times_{f} X) ↾}_{A} = T \times_{f} X$
292	290 291	syl	$⊢ φ \to {(T \times_{f} X) ↾}_{A} = T \times_{f} X$
293	292	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A}) = \sum_{ℂ_{fld}} (T \times_{f} X)$
294	293 12	oveq12d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} = \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}$
295	9 258 4 4 155	offn	$⊢ φ \to (T \times_{f} (F \circ X)) Fn A$
296		fnresdm	$⊢ (T \times_{f} (F \circ X)) Fn A \to {(T \times_{f} (F \circ X)) ↾}_{A} = T \times_{f} (F \circ X)$
297	295 296	syl	$⊢ φ \to {(T \times_{f} (F \circ X)) ↾}_{A} = T \times_{f} (F \circ X)$
298	297	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A}) = \sum_{ℂ_{fld}} (T \times_{f} (F \circ X))$
299	298 12	oveq12d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} = \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}$
300	299	breq2d	$⊢ φ \to (F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})} \leftrightarrow F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$
301	300	rabbidv	$⊢ φ \to \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{A})}{\sum_{ℂ_{fld}} ({T ↾}_{A})}\} = \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}\}$
302	289 294 301	3eltr3d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}\}$
303		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \to F (w) = F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T})$
304	303	breq1d	$⊢ w = \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \to (F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T} \leftrightarrow F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$
305	304	elrab	$⊢ \frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in \{w \in D \| F (w) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T}\} \leftrightarrow (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in D \land F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$
306	302 305	sylib	$⊢ φ \to (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T} \in D \land F (\frac{\sum_{ℂ_{fld}} (T \times_{f} X)}{\sum_{ℂ_{fld}} T}) \leq \frac{\sum_{ℂ_{fld}} (T \times_{f} (F \circ X))}{\sum_{ℂ_{fld}} T})$

Metamath Proof Explorer

Theorem jensen

Proof