ex-fpar

Description: Formalized example provided in the comment for fpar . (Contributed by AV, 3-Jan-2024)

	Ref	Expression
Hypotheses	ex-fpar.h	$⊢ H = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)})))$
	ex-fpar.a	$⊢ A = [0, +∞)$
	ex-fpar.b	$⊢ B = ℝ$
	ex-fpar.f	$⊢ F = {\sqrt ↾}_{A}$
	ex-fpar.g	$⊢ G = {\sin ↾}_{B}$
Assertion	ex-fpar	$⊢ (X \in A \land Y \in B) \to X (+ \circ H) Y = \sqrt{X} + \sin Y$

Proof

Step	Hyp	Ref	Expression
1		ex-fpar.h	$⊢ H = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (F \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (G \circ ({2^{nd} ↾}_{(V \times V)})))$
2		ex-fpar.a	$⊢ A = [0, +∞)$
3		ex-fpar.b	$⊢ B = ℝ$
4		ex-fpar.f	$⊢ F = {\sqrt ↾}_{A}$
5		ex-fpar.g	$⊢ G = {\sin ↾}_{B}$
6		df-ov	$⊢ X (+ \circ H) Y = (+ \circ H) (⟨X, Y⟩)$
7		sqrtf	$⊢ \sqrt : ℂ ⟶ ℂ$
8		ffn	$⊢ \sqrt : ℂ ⟶ ℂ \to \sqrt Fn ℂ$
9	7 8	ax-mp	$⊢ \sqrt Fn ℂ$
10		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
11		ax-resscn	$⊢ ℝ \subseteq ℂ$
12	10 11	sstri	$⊢ [0, +∞) \subseteq ℂ$
13		fnssres	$⊢ (\sqrt Fn ℂ \land [0, +∞) \subseteq ℂ) \to ({\sqrt ↾}_{[0, +∞)}) Fn [0, +∞)$
14	2	reseq2i	$⊢ {\sqrt ↾}_{A} = {\sqrt ↾}_{[0, +∞)}$
15	14	fneq1i	$⊢ ({\sqrt ↾}_{A}) Fn [0, +∞) \leftrightarrow ({\sqrt ↾}_{[0, +∞)}) Fn [0, +∞)$
16	13 15	sylibr	$⊢ (\sqrt Fn ℂ \land [0, +∞) \subseteq ℂ) \to ({\sqrt ↾}_{A}) Fn [0, +∞)$
17	9 12 16	mp2an	$⊢ ({\sqrt ↾}_{A}) Fn [0, +∞)$
18		id	$⊢ F = {\sqrt ↾}_{A} \to F = {\sqrt ↾}_{A}$
19	2	a1i	$⊢ F = {\sqrt ↾}_{A} \to A = [0, +∞)$
20	18 19	fneq12d	$⊢ F = {\sqrt ↾}_{A} \to (F Fn A \leftrightarrow ({\sqrt ↾}_{A}) Fn [0, +∞))$
21	4 20	ax-mp	$⊢ F Fn A \leftrightarrow ({\sqrt ↾}_{A}) Fn [0, +∞)$
22	17 21	mpbir	$⊢ F Fn A$
23		sinf	$⊢ \sin : ℂ ⟶ ℂ$
24		ffn	$⊢ \sin : ℂ ⟶ ℂ \to \sin Fn ℂ$
25	23 24	ax-mp	$⊢ \sin Fn ℂ$
26		fnssres	$⊢ (\sin Fn ℂ \land ℝ \subseteq ℂ) \to ({\sin ↾}_{ℝ}) Fn ℝ$
27	3	reseq2i	$⊢ {\sin ↾}_{B} = {\sin ↾}_{ℝ}$
28	27	fneq1i	$⊢ ({\sin ↾}_{B}) Fn ℝ \leftrightarrow ({\sin ↾}_{ℝ}) Fn ℝ$
29	26 28	sylibr	$⊢ (\sin Fn ℂ \land ℝ \subseteq ℂ) \to ({\sin ↾}_{B}) Fn ℝ$
30	25 11 29	mp2an	$⊢ ({\sin ↾}_{B}) Fn ℝ$
31		id	$⊢ G = {\sin ↾}_{B} \to G = {\sin ↾}_{B}$
32	3	a1i	$⊢ G = {\sin ↾}_{B} \to B = ℝ$
33	31 32	fneq12d	$⊢ G = {\sin ↾}_{B} \to (G Fn B \leftrightarrow ({\sin ↾}_{B}) Fn ℝ)$
34	5 33	ax-mp	$⊢ G Fn B \leftrightarrow ({\sin ↾}_{B}) Fn ℝ$
35	30 34	mpbir	$⊢ G Fn B$
36	1	fpar	$⊢ (F Fn A \land G Fn B) \to H = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$
37	22 35 36	mp2an	$⊢ H = (x \in A, y \in B ⟼ ⟨F (x), G (y)⟩)$
38		opex	$⊢ ⟨F (x), G (y)⟩ \in V$
39	37 38	fnmpoi	$⊢ H Fn (A \times B)$
40		opelxpi	$⊢ (X \in A \land Y \in B) \to ⟨X, Y⟩ \in (A \times B)$
41		fvco2	$⊢ (H Fn (A \times B) \land ⟨X, Y⟩ \in (A \times B)) \to (+ \circ H) (⟨X, Y⟩) = + (H (⟨X, Y⟩))$
42	39 40 41	sylancr	$⊢ (X \in A \land Y \in B) \to (+ \circ H) (⟨X, Y⟩) = + (H (⟨X, Y⟩))$
43		simpl	$⊢ (X \in A \land Y \in B) \to X \in A$
44		simpr	$⊢ (X \in A \land Y \in B) \to Y \in B$
45	37 43 44	fvproj	$⊢ (X \in A \land Y \in B) \to H (⟨X, Y⟩) = ⟨F (X), G (Y)⟩$
46	45	fveq2d	$⊢ (X \in A \land Y \in B) \to + (H (⟨X, Y⟩)) = + (⟨F (X), G (Y)⟩)$
47		df-ov	$⊢ F (X) + G (Y) = + (⟨F (X), G (Y)⟩)$
48	4	fveq1i	$⊢ F (X) = ({\sqrt ↾}_{A}) (X)$
49		fvres	$⊢ X \in A \to ({\sqrt ↾}_{A}) (X) = \sqrt{X}$
50	48 49	eqtrid	$⊢ X \in A \to F (X) = \sqrt{X}$
51	5	fveq1i	$⊢ G (Y) = ({\sin ↾}_{B}) (Y)$
52		fvres	$⊢ Y \in B \to ({\sin ↾}_{B}) (Y) = \sin Y$
53	51 52	eqtrid	$⊢ Y \in B \to G (Y) = \sin Y$
54	50 53	oveqan12d	$⊢ (X \in A \land Y \in B) \to F (X) + G (Y) = \sqrt{X} + \sin Y$
55	47 54	eqtr3id	$⊢ (X \in A \land Y \in B) \to + (⟨F (X), G (Y)⟩) = \sqrt{X} + \sin Y$
56	42 46 55	3eqtrd	$⊢ (X \in A \land Y \in B) \to (+ \circ H) (⟨X, Y⟩) = \sqrt{X} + \sin Y$
57	6 56	eqtrid	$⊢ (X \in A \land Y \in B) \to X (+ \circ H) Y = \sqrt{X} + \sin Y$

Metamath Proof Explorer

Theorem ex-fpar

Proof