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 ‘ 𝑌 ) ) )