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	syl5eq	⊢ ( ¬ 𝑊 ∈ 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	⊢ · = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 , 𝑦 ) )