Metamath Proof Explorer

Theorem asclfval

Description: Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclfval.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
asclfval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
asclfval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
asclfval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
asclfval.o ⊢ 1 = ( 1r ‘ 𝑊 )
Assertion asclfval 𝐴 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) )

Proof

Step Hyp Ref Expression
1 asclfval.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 asclfval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 asclfval.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 asclfval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 asclfval.o ⊢ 1 = ( 1r ‘ 𝑊 )
6 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
7 6 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
8 7 fveq2d ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝐹 ) )
9 8 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝐾 )
10 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
11 10 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
12 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 )
13 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 1r ‘ 𝑤 ) = ( 1r ‘ 𝑊 ) )
14 13 5 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 1r ‘ 𝑤 ) = 1 )
15 11 12 14 oveq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) = ( 𝑥 · 1 ) )
16 9 15 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) ) )
17 df-ascl ⊢ algSc = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑤 ) ( 1r ‘ 𝑤 ) ) ) )
18 16 17 3 mptfvmpt ⊢ ( 𝑊 ∈ V → ( algSc ‘ 𝑊 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) ) )
19 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( algSc ‘ 𝑊 ) = ∅ )
20 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( 𝑥 · 1 ) ) = ∅
21 19 20 eqtr4di ⊢ ( ¬ 𝑊 ∈ V → ( algSc ‘ 𝑊 ) = ( 𝑥 ∈ ∅ ↦ ( 𝑥 · 1 ) ) )
22 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( Scalar ‘ 𝑊 ) = ∅ )
23 2 22 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐹 = ∅ )
24 23 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝐹 ) = ( Base ‘ ∅ ) )
25 base0 ⊢ ∅ = ( Base ‘ ∅ )
26 24 25 eqtr4di ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝐹 ) = ∅ )
27 3 26 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
28 27 mpteq1d ⊢ ( ¬ 𝑊 ∈ V → ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑥 · 1 ) ) )
29 21 28 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( algSc ‘ 𝑊 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) ) )
30 18 29 pm2.61i ⊢ ( algSc ‘ 𝑊 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) )
31 1 30 eqtri ⊢ 𝐴 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 · 1 ) )