Metamath Proof Explorer

Theorem sravsca

Description: The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Proof shortened by AV, 12-Nov-2024)

Ref Expression
Hypotheses srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion sravsca ( 𝜑 → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2 srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3 ovex ⊢ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ∈ V
4 fvex ⊢ ( .r ‘ 𝑊 ) ∈ V
5 vscaid ⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
6 5 setsid ⊢ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ∈ V ∧ ( .r ‘ 𝑊 ) ∈ V ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
7 3 4 6 mp2an ⊢ ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
8 slotsdifipndx ⊢ ( ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ∧ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
9 8 simpli ⊢ ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
10 5 9 setsnid ⊢ ( ·𝑠 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) = ( ·𝑠 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
11 7 10 eqtri ⊢ ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
12 1 adantl ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
13 sraval ⊢ ( ( 𝑊 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
14 2 13 sylan2 ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
15 12 14 eqtrd ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
16 15 fveq2d ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
17 11 16 eqtr4id ⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
18 5 str0 ⊢ ∅ = ( ·𝑠 ‘ ∅ )
19 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( .r ‘ 𝑊 ) = ∅ )
20 19 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( .r ‘ 𝑊 ) = ∅ )
21 fv2prc ⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
22 1 21 sylan9eqr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
23 22 fveq2d ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ∅ ) )
24 18 20 23 3eqtr4a ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )
25 17 24 pm2.61ian ⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐴 ) )