Metamath Proof Explorer

Theorem ipffval

Description: The inner product operation as a function. (Contributed by Mario Carneiro, 12-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses ipffval.1 
|- V = ( Base ` W )
ipffval.2 
|- ., = ( .i ` W )
ipffval.3 
|- .x. = ( .if ` W )
Assertion ipffval 
|- .x. = ( x e. V , y e. V |-> ( x ., y ) )

Proof

Step Hyp Ref Expression
1 ipffval.1 
 |-  V = ( Base ` W )
2 ipffval.2 
 |-  ., = ( .i ` W )
3 ipffval.3 
 |-  .x. = ( .if ` W )
4 fveq2 
 |-  ( g = W -> ( Base ` g ) = ( Base ` W ) )
5 4 1 eqtr4di 
 |-  ( g = W -> ( Base ` g ) = V )
6 fveq2 
 |-  ( g = W -> ( .i ` g ) = ( .i ` W ) )
7 6 2 eqtr4di 
 |-  ( g = W -> ( .i ` g ) = ., )
8 7 oveqd 
 |-  ( g = W -> ( x ( .i ` g ) y ) = ( x ., y ) )
9 5 5 8 mpoeq123dv 
 |-  ( g = W -> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( .i ` g ) y ) ) = ( x e. V , y e. V |-> ( x ., y ) ) )
10 df-ipf 
 |-  .if = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( .i ` g ) y ) ) )
11 1 fvexi 
 |-  V e. _V
12 2 fvexi 
 |-  ., e. _V
13 12 rnex 
 |-  ran ., e. _V
14 p0ex 
 |-  { (/) } e. _V
15 13 14 unex 
 |-  ( ran ., u. { (/) } ) e. _V
16 df-ov 
 |-  ( x ., y ) = ( ., ` <. x , y >. )
17 fvrn0 
 |-  ( ., ` <. x , y >. ) e. ( ran ., u. { (/) } )
18 16 17 eqeltri 
 |-  ( x ., y ) e. ( ran ., u. { (/) } )
19 18 rgen2w 
 |-  A. x e. V A. y e. V ( x ., y ) e. ( ran ., u. { (/) } )
20 11 11 15 19 mpoexw 
 |-  ( x e. V , y e. V |-> ( x ., y ) ) e. _V
21 9 10 20 fvmpt 
 |-  ( W e. _V -> ( .if ` W ) = ( x e. V , y e. V |-> ( x ., y ) ) )
22 fvprc 
 |-  ( -. W e. _V -> ( .if ` W ) = (/) )
23 fvprc 
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
24 1 23 syl5eq 
 |-  ( -. W e. _V -> V = (/) )
25 24 olcd 
 |-  ( -. W e. _V -> ( V = (/) \/ V = (/) ) )
26 0mpo0 
 |-  ( ( V = (/) \/ V = (/) ) -> ( x e. V , y e. V |-> ( x ., y ) ) = (/) )
27 25 26 syl 
 |-  ( -. W e. _V -> ( x e. V , y e. V |-> ( x ., y ) ) = (/) )
28 22 27 eqtr4d 
 |-  ( -. W e. _V -> ( .if ` W ) = ( x e. V , y e. V |-> ( x ., y ) ) )
29 21 28 pm2.61i 
 |-  ( .if ` W ) = ( x e. V , y e. V |-> ( x ., y ) )
30 3 29 eqtri 
 |-  .x. = ( x e. V , y e. V |-> ( x ., y ) )