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 ⊢ φ → A = subringAlg ⁡ W ⁡ S
srapart.s ⊢ φ → S ⊆ Base W
Assertion sravsca ⊢ φ → ⋅ W = ⋅ A

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 srapart.s ⊢ φ → S ⊆ Base W
3 ovex ⊢ W sSet Scalar ⁡ ndx W ↾ 𝑠 S ∈ V
4 fvex ⊢ ⋅ W ∈ V
5 vscaid ⊢ ⋅ 𝑠 = Slot ⋅ ndx
6 5 setsid ⊢ W sSet Scalar ⁡ ndx W ↾ 𝑠 S ∈ V ∧ ⋅ W ∈ V → ⋅ W = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W
7 3 4 6 mp2an ⊢ ⋅ W = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W
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 ⊢ ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
16 7 15 eqtri ⊢ ⋅ W = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
17 1 adantl ⊢ W ∈ V ∧ φ → A = subringAlg ⁡ W ⁡ S
18 sraval ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
19 2 18 sylan2 ⊢ W ∈ V ∧ φ → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
20 17 19 eqtrd ⊢ W ∈ V ∧ φ → A = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
21 20 fveq2d ⊢ W ∈ V ∧ φ → ⋅ A = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
22 16 21 eqtr4id ⊢ W ∈ V ∧ φ → ⋅ W = ⋅ A
23 5 str0 ⊢ ∅ = ⋅ ∅
24 fvprc ⊢ ¬ W ∈ V → ⋅ W = ∅
25 24 adantr ⊢ ¬ W ∈ V ∧ φ → ⋅ W = ∅
26 fv2prc ⊢ ¬ W ∈ V → subringAlg ⁡ W ⁡ S = ∅
27 1 26 sylan9eqr ⊢ ¬ W ∈ V ∧ φ → A = ∅
28 27 fveq2d ⊢ ¬ W ∈ V ∧ φ → ⋅ A = ⋅ ∅
29 23 25 28 3eqtr4a ⊢ ¬ W ∈ V ∧ φ → ⋅ W = ⋅ A
30 22 29 pm2.61ian ⊢ φ → ⋅ W = ⋅ A