This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipffval.2 ⊢ , = ( ·𝑖 ‘ 𝑊 )
ipffval.3 ⊢ · = ( ·if ‘ 𝑊 )
Assertion ipffval · = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) )

Proof

Step Hyp Ref Expression
1 ipffval.1 ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ipffval.2 ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 ipffval.3 ⊢ · = ( ·if ‘ 𝑊 )
4 fveq2 ⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑊 ) )
5 4 1 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) = 𝑉 )
6 fveq2 ⊢ ( 𝑔 = 𝑊 → ( ·𝑖 ‘ 𝑔 ) = ( ·𝑖 ‘ 𝑊 ) )
7 6 2 eqtr4di ⊢ ( 𝑔 = 𝑊 → ( ·𝑖 ‘ 𝑔 ) = , )
8 7 oveqd ⊢ ( 𝑔 = 𝑊 → ( 𝑥 ( ·𝑖 ‘ 𝑔 ) 𝑦 ) = ( 𝑥 , 𝑦 ) )
9 5 5 8 mpoeq123dv ⊢ ( 𝑔 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑔 ) 𝑦 ) ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) )
10 df-ipf ⊢ ·if = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑔 ) 𝑦 ) ) )
11 1 fvexi ⊢ 𝑉 ∈ V
12 2 fvexi ⊢ , ∈ V
13 12 rnex ⊢ ran , ∈ V
14 p0ex ⊢ { ∅ } ∈ V
15 13 14 unex ⊢ ( ran , ∪ { ∅ } ) ∈ V
16 df-ov ⊢ ( 𝑥 , 𝑦 ) = ( , ‘ ⟨ 𝑥 , 𝑦 ⟩ )
17 fvrn0 ⊢ ( , ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ran , ∪ { ∅ } )
18 16 17 eqeltri ⊢ ( 𝑥 , 𝑦 ) ∈ ( ran , ∪ { ∅ } )
19 18 rgen2w ⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 , 𝑦 ) ∈ ( ran , ∪ { ∅ } )
20 11 11 15 19 mpoexw ⊢ ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) ∈ V
21 9 10 20 fvmpt ⊢ ( 𝑊 ∈ V → ( ·if ‘ 𝑊 ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) )
22 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( ·if ‘ 𝑊 ) = ∅ )
23 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
24 1 23 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝑉 = ∅ )
25 24 olcd ⊢ ( ¬ 𝑊 ∈ V → ( 𝑉 = ∅ ∨ 𝑉 = ∅ ) )
26 0mpo0 ⊢ ( ( 𝑉 = ∅ ∨ 𝑉 = ∅ ) → ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) = ∅ )
27 25 26 syl ⊢ ( ¬ 𝑊 ∈ V → ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) = ∅ )
28 22 27 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( ·if ‘ 𝑊 ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) ) )
29 21 28 pm2.61i ⊢ ( ·if ‘ 𝑊 ) = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) )
30 3 29 eqtri ⊢ · = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) )