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 
|- H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
ex-fpar.a 
|- A = ( 0 [,) +oo )
ex-fpar.b 
|- B = RR
ex-fpar.f 
|- F = ( sqrt |` A )
ex-fpar.g 
|- G = ( sin |` B )
Assertion ex-fpar 
|- ( ( X e. A /\ Y e. B ) -> ( X ( + o. H ) Y ) = ( ( sqrt ` X ) + ( sin ` Y ) ) )

Proof

Step Hyp Ref Expression
1 ex-fpar.h 
 |-  H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
2 ex-fpar.a 
 |-  A = ( 0 [,) +oo )
3 ex-fpar.b 
 |-  B = RR
4 ex-fpar.f 
 |-  F = ( sqrt |` A )
5 ex-fpar.g 
 |-  G = ( sin |` B )
6 df-ov 
 |-  ( X ( + o. H ) Y ) = ( ( + o. H ) ` <. X , Y >. )
7 sqrtf 
 |-  sqrt : CC --> CC
8 ffn 
 |-  ( sqrt : CC --> CC -> sqrt Fn CC )
9 7 8 ax-mp 
 |-  sqrt Fn CC
10 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
11 ax-resscn 
 |-  RR C_ CC
12 10 11 sstri 
 |-  ( 0 [,) +oo ) C_ CC
13 fnssres 
 |-  ( ( sqrt Fn CC /\ ( 0 [,) +oo ) C_ CC ) -> ( sqrt |` ( 0 [,) +oo ) ) Fn ( 0 [,) +oo ) )
14 2 reseq2i 
 |-  ( sqrt |` A ) = ( sqrt |` ( 0 [,) +oo ) )
15 14 fneq1i 
 |-  ( ( sqrt |` A ) Fn ( 0 [,) +oo ) <-> ( sqrt |` ( 0 [,) +oo ) ) Fn ( 0 [,) +oo ) )
16 13 15 sylibr 
 |-  ( ( sqrt Fn CC /\ ( 0 [,) +oo ) C_ CC ) -> ( sqrt |` A ) Fn ( 0 [,) +oo ) )
17 9 12 16 mp2an 
 |-  ( sqrt |` A ) Fn ( 0 [,) +oo )
18 id 
 |-  ( F = ( sqrt |` A ) -> F = ( sqrt |` A ) )
19 2 a1i 
 |-  ( F = ( sqrt |` A ) -> A = ( 0 [,) +oo ) )
20 18 19 fneq12d 
 |-  ( F = ( sqrt |` A ) -> ( F Fn A <-> ( sqrt |` A ) Fn ( 0 [,) +oo ) ) )
21 4 20 ax-mp 
 |-  ( F Fn A <-> ( sqrt |` A ) Fn ( 0 [,) +oo ) )
22 17 21 mpbir 
 |-  F Fn A
23 sinf 
 |-  sin : CC --> CC
24 ffn 
 |-  ( sin : CC --> CC -> sin Fn CC )
25 23 24 ax-mp 
 |-  sin Fn CC
26 fnssres 
 |-  ( ( sin Fn CC /\ RR C_ CC ) -> ( sin |` RR ) Fn RR )
27 3 reseq2i 
 |-  ( sin |` B ) = ( sin |` RR )
28 27 fneq1i 
 |-  ( ( sin |` B ) Fn RR <-> ( sin |` RR ) Fn RR )
29 26 28 sylibr 
 |-  ( ( sin Fn CC /\ RR C_ CC ) -> ( sin |` B ) Fn RR )
30 25 11 29 mp2an 
 |-  ( sin |` B ) Fn RR
31 id 
 |-  ( G = ( sin |` B ) -> G = ( sin |` B ) )
32 3 a1i 
 |-  ( G = ( sin |` B ) -> B = RR )
33 31 32 fneq12d 
 |-  ( G = ( sin |` B ) -> ( G Fn B <-> ( sin |` B ) Fn RR ) )
34 5 33 ax-mp 
 |-  ( G Fn B <-> ( sin |` B ) Fn RR )
35 30 34 mpbir 
 |-  G Fn B
36 1 fpar 
 |-  ( ( F Fn A /\ G Fn B ) -> H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) )
37 22 35 36 mp2an 
 |-  H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )
38 opex 
 |-  <. ( F ` x ) , ( G ` y ) >. e. _V
39 37 38 fnmpoi 
 |-  H Fn ( A X. B )
40 opelxpi 
 |-  ( ( X e. A /\ Y e. B ) -> <. X , Y >. e. ( A X. B ) )
41 fvco2 
 |-  ( ( H Fn ( A X. B ) /\ <. X , Y >. e. ( A X. B ) ) -> ( ( + o. H ) ` <. X , Y >. ) = ( + ` ( H ` <. X , Y >. ) ) )
42 39 40 41 sylancr 
 |-  ( ( X e. A /\ Y e. B ) -> ( ( + o. H ) ` <. X , Y >. ) = ( + ` ( H ` <. X , Y >. ) ) )
43 simpl 
 |-  ( ( X e. A /\ Y e. B ) -> X e. A )
44 simpr 
 |-  ( ( X e. A /\ Y e. B ) -> Y e. B )
45 37 43 44 fvproj 
 |-  ( ( X e. A /\ Y e. B ) -> ( H ` <. X , Y >. ) = <. ( F ` X ) , ( G ` Y ) >. )
46 45 fveq2d 
 |-  ( ( X e. A /\ Y e. B ) -> ( + ` ( 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 e. A -> ( ( sqrt |` A ) ` X ) = ( sqrt ` X ) )
50 48 49 eqtrid 
 |-  ( X e. A -> ( F ` X ) = ( sqrt ` X ) )
51 5 fveq1i 
 |-  ( G ` Y ) = ( ( sin |` B ) ` Y )
52 fvres 
 |-  ( Y e. B -> ( ( sin |` B ) ` Y ) = ( sin ` Y ) )
53 51 52 eqtrid 
 |-  ( Y e. B -> ( G ` Y ) = ( sin ` Y ) )
54 50 53 oveqan12d 
 |-  ( ( X e. A /\ Y e. B ) -> ( ( F ` X ) + ( G ` Y ) ) = ( ( sqrt ` X ) + ( sin ` Y ) ) )
55 47 54 eqtr3id 
 |-  ( ( X e. A /\ Y e. B ) -> ( + ` <. ( F ` X ) , ( G ` Y ) >. ) = ( ( sqrt ` X ) + ( sin ` Y ) ) )
56 42 46 55 3eqtrd 
 |-  ( ( X e. A /\ Y e. B ) -> ( ( + o. H ) ` <. X , Y >. ) = ( ( sqrt ` X ) + ( sin ` Y ) ) )
57 6 56 eqtrid 
 |-  ( ( X e. A /\ Y e. B ) -> ( X ( + o. H ) Y ) = ( ( sqrt ` X ) + ( sin ` Y ) ) )