Metamath Proof Explorer

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