Theorem scaffval

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

	Ref	Expression
Hypotheses	scaffval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	scaffval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	scaffval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	scaffval.a	⊢ ∙ = ( ·sf ‘ 𝑊 )
	scaffval.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion	scaffval	⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		scaffval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		scaffval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		scaffval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
4		scaffval.a	⊢ ∙ = ( ·sf ‘ 𝑊 )
5		scaffval.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
7	6 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
8	7	fveq2d	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝐹 ) )
9	8 3	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝐾 )
10		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
11	10 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
12		fveq2	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
13	12 5	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
14	13	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
15	9 11 14	mpoeq123dv	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) )
16		df-scaf	⊢ ·sf = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) , 𝑦 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) 𝑦 ) ) )
17	3	fvexi	⊢ 𝐾 ∈ V
18	1	fvexi	⊢ 𝐵 ∈ V
19	5	fvexi	⊢ · ∈ V
20	19	rnex	⊢ ran · ∈ V
21		p0ex	⊢ { ∅ } ∈ V
22	20 21	unex	⊢ ( ran · ∪ { ∅ } ) ∈ V
23		df-ov	⊢ ( 𝑥 · 𝑦 ) = ( · ‘ ⟨ 𝑥 , 𝑦 ⟩ )
24		fvrn0	⊢ ( · ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ran · ∪ { ∅ } )
25	23 24	eqeltri	⊢ ( 𝑥 · 𝑦 ) ∈ ( ran · ∪ { ∅ } )
26	25	rgen2w	⊢ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) ∈ ( ran · ∪ { ∅ } )
27	17 18 22 26	mpoexw	⊢ ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) ∈ V
28	15 16 27	fvmpt	⊢ ( 𝑊 ∈ V → ( ·sf ‘ 𝑊 ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) )
29		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( ·sf ‘ 𝑊 ) = ∅ )
30		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
31	1 30	eqtrid	⊢ ( ¬ 𝑊 ∈ V → 𝐵 = ∅ )
32	31	olcd	⊢ ( ¬ 𝑊 ∈ V → ( 𝐾 = ∅ ∨ 𝐵 = ∅ ) )
33		0mpo0	⊢ ( ( 𝐾 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) = ∅ )
34	32 33	syl	⊢ ( ¬ 𝑊 ∈ V → ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) = ∅ )
35	29 34	eqtr4d	⊢ ( ¬ 𝑊 ∈ V → ( ·sf ‘ 𝑊 ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) )
36	28 35	pm2.61i	⊢ ( ·sf ‘ 𝑊 ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) )
37	4 36	eqtri	⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) )