Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) = ( √ ‘ 𝑋 ) )
51 5 fveq1i ⊢ ( 𝐺 ‘ 𝑌 ) = ( ( sin ↾ 𝐵 ) ‘ 𝑌 )
52 fvres ⊢ ( 𝑌 ∈ 𝐵 → ( ( sin ↾ 𝐵 ) ‘ 𝑌 ) = ( sin ‘ 𝑌 ) )
53 51 52 syl5eq ⊢ ( 𝑌 ∈ 𝐵 → ( 𝐺 ‘ 𝑌 ) = ( sin ‘ 𝑌 ) )
54 50 53 oveqan12d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐺 ‘ 𝑌 ) ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )
55 47 54 eqtr3id ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( + ‘ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )
56 42 46 55 3eqtrd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ( + ∘ 𝐻 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )
57 6 56 syl5eq ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( + ∘ 𝐻 ) 𝑌 ) = ( ( √ ‘ 𝑋 ) + ( sin ‘ 𝑌 ) ) )