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)

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 6re 6 ∈ ℝ
9 6lt8 6 < 8
10 8 9 ltneii 6 ≠ 8
11 vscandx ( ·𝑠 ‘ ndx ) = 6
12 ipndx ( ·𝑖 ‘ ndx ) = 8
13 11 12 neeq12i ( ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ 6 ≠ 8 )
14 10 13 mpbir ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
15 5 14 setsnid ( ·𝑠 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) ) = ( ·𝑠 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r𝑊 ) ⟩ ) )
16 7 15 eqtri ( .r𝑊 ) = ( ·𝑠 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r𝑊 ) ⟩ ) )
17 1 adantl ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
18 sraval ( ( 𝑊 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r𝑊 ) ⟩ ) )
19 2 18 sylan2 ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r𝑊 ) ⟩ ) )
20 17 19 eqtrd ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r𝑊 ) ⟩ ) )
21 20 fveq2d ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ·𝑠𝐴 ) = ( ·𝑠 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r𝑊 ) ⟩ ) ) )
22 16 21 eqtr4id ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( .r𝑊 ) = ( ·𝑠𝐴 ) )
23 5 str0 ∅ = ( ·𝑠 ‘ ∅ )
24 fvprc ( ¬ 𝑊 ∈ V → ( .r𝑊 ) = ∅ )
25 24 adantr ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( .r𝑊 ) = ∅ )
26 fv2prc ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
27 1 26 sylan9eqr ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
28 27 fveq2d ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( ·𝑠𝐴 ) = ( ·𝑠 ‘ ∅ ) )
29 23 25 28 3eqtr4a ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( .r𝑊 ) = ( ·𝑠𝐴 ) )
30 22 29 pm2.61ian ( 𝜑 → ( .r𝑊 ) = ( ·𝑠𝐴 ) )