Theorem ex-fpar

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

	Ref	Expression
Hypotheses	ex-fpar.h	⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
	ex-fpar.a	⊢ 𝐴 = ( 0 [,) +∞ )
	ex-fpar.b	⊢ 𝐵 = ℝ
	ex-fpar.f	⊢ 𝐹 = ( √ ↾ 𝐴 )
	ex-fpar.g	⊢ 𝐺 = ( sin ↾ 𝐵 )
Assertion	ex-fpar	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( + ∘ 𝐻 ) 𝑌 ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ex-fpar.h	⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
2		ex-fpar.a	⊢ 𝐴 = ( 0 [,) +∞ )
3		ex-fpar.b	⊢ 𝐵 = ℝ
4		ex-fpar.f	⊢ 𝐹 = ( √ ↾ 𝐴 )
5		ex-fpar.g	⊢ 𝐺 = ( sin ↾ 𝐵 )
6		df-ov	⊢ ( 𝑋 ( + ∘ 𝐻 ) 𝑌 ) = ( ( + ∘ 𝐻 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
7		sqrtf	⊢ √ : ℂ ⟶ ℂ
8		ffn	⊢ ( √ : ℂ ⟶ ℂ → √ Fn ℂ )
9	7 8	ax-mp	⊢ √ Fn ℂ
10		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
11		ax-resscn	⊢ ℝ ⊆ ℂ
12	10 11	sstri	⊢ ( 0 [,) +∞ ) ⊆ ℂ
13		fnssres	⊢ ( ( √ Fn ℂ ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → ( √ ↾ ( 0 [,) +∞ ) ) Fn ( 0 [,) +∞ ) )
14	2	reseq2i	⊢ ( √ ↾ 𝐴 ) = ( √ ↾ ( 0 [,) +∞ ) )
15	14	fneq1i	⊢ ( ( √ ↾ 𝐴 ) Fn ( 0 [,) +∞ ) ↔ ( √ ↾ ( 0 [,) +∞ ) ) Fn ( 0 [,) +∞ ) )
16	13 15	sylibr	⊢ ( ( √ Fn ℂ ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → ( √ ↾ 𝐴 ) Fn ( 0 [,) +∞ ) )
17	9 12 16	mp2an	⊢ ( √ ↾ 𝐴 ) Fn ( 0 [,) +∞ )
18		id	⊢ ( 𝐹 = ( √ ↾ 𝐴 ) → 𝐹 = ( √ ↾ 𝐴 ) )
19	2	a1i	⊢ ( 𝐹 = ( √ ↾ 𝐴 ) → 𝐴 = ( 0 [,) +∞ ) )
20	18 19	fneq12d	⊢ ( 𝐹 = ( √ ↾ 𝐴 ) → ( 𝐹 Fn 𝐴 ↔ ( √ ↾ 𝐴 ) Fn ( 0 [,) +∞ ) ) )
21	4 20	ax-mp	⊢ ( 𝐹 Fn 𝐴 ↔ ( √ ↾ 𝐴 ) Fn ( 0 [,) +∞ ) )
22	17 21	mpbir	⊢ 𝐹 Fn 𝐴
23		sinf	⊢ sin : ℂ ⟶ ℂ
24		ffn	⊢ ( sin : ℂ ⟶ ℂ → sin Fn ℂ )
25	23 24	ax-mp	⊢ sin Fn ℂ
26		fnssres	⊢ ( ( sin Fn ℂ ∧ ℝ ⊆ ℂ ) → ( sin ↾ ℝ ) Fn ℝ )
27	3	reseq2i	⊢ ( sin ↾ 𝐵 ) = ( sin ↾ ℝ )
28	27	fneq1i	⊢ ( ( sin ↾ 𝐵 ) Fn ℝ ↔ ( sin ↾ ℝ ) Fn ℝ )
29	26 28	sylibr	⊢ ( ( sin Fn ℂ ∧ ℝ ⊆ ℂ ) → ( sin ↾ 𝐵 ) Fn ℝ )
30	25 11 29	mp2an	⊢ ( sin ↾ 𝐵 ) Fn ℝ
31		id	⊢ ( 𝐺 = ( sin ↾ 𝐵 ) → 𝐺 = ( sin ↾ 𝐵 ) )
32	3	a1i	⊢ ( 𝐺 = ( sin ↾ 𝐵 ) → 𝐵 = ℝ )
33	31 32	fneq12d	⊢ ( 𝐺 = ( sin ↾ 𝐵 ) → ( 𝐺 Fn 𝐵 ↔ ( sin ↾ 𝐵 ) Fn ℝ ) )
34	5 33	ax-mp	⊢ ( 𝐺 Fn 𝐵 ↔ ( sin ↾ 𝐵 ) Fn ℝ )
35	30 34	mpbir	⊢ 𝐺 Fn 𝐵
36	1	fpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) )
37	22 35 36	mp2an	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
38		opex	⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V
39	37 38	fnmpoi	⊢ 𝐻 Fn ( 𝐴 × 𝐵 )
40		opelxpi	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
41		fvco2	⊢ ( ( 𝐻 Fn ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( ( + ∘ 𝐻 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( + ‘ ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
42	39 40 41	sylancr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( + ∘ 𝐻 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( + ‘ ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
43		simpl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
44		simpr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
45	37 43 44	fvproj	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )
46	45	fveq2d	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( + ‘ ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( + ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ ) )
47		df-ov	⊢ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐺 ‘ 𝑌 ) ) = ( + ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )
48	4	fveq1i	⊢ ( 𝐹 ‘ 𝑋 ) = ( ( √ ↾ 𝐴 ) ‘ 𝑋 )
49		fvres	⊢ ( 𝑋 ∈ 𝐴 → ( ( √ ↾ 𝐴 ) ‘ 𝑋 ) = ( √ ‘ 𝑋 ) )
50	48 49	eqtrid	⊢ ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) = ( √ ‘ 𝑋 ) )
51	5	fveq1i	⊢ ( 𝐺 ‘ 𝑌 ) = ( ( sin ↾ 𝐵 ) ‘ 𝑌 )
52		fvres	⊢ ( 𝑌 ∈ 𝐵 → ( ( sin ↾ 𝐵 ) ‘ 𝑌 ) = ( sin ‘ 𝑌 ) )
53	51 52	eqtrid	⊢ ( 𝑌 ∈ 𝐵 → ( 𝐺 ‘ 𝑌 ) = ( sin ‘ 𝑌 ) )
54	50 53	oveqan12d	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐺 ‘ 𝑌 ) ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )
55	47 54	eqtr3id	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( + ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )
56	42 46 55	3eqtrd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( + ∘ 𝐻 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )
57	6 56	eqtrid	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( + ∘ 𝐻 ) 𝑌 ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )