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 ⊢ φ → 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 slotsdifipndx ⊢ ⋅ ndx ≠ ⋅ 𝑖 ⁡ ndx ∧ Scalar ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
9 8 simpli ⊢ ⋅ ndx ≠ ⋅ 𝑖 ⁡ ndx
10 5 9 setsnid ⊢ ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
11 7 10 eqtri ⊢ ⋅ W = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
12 1 adantl ⊢ W ∈ V ∧ φ → A = subringAlg ⁡ W ⁡ S
13 sraval ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
14 2 13 sylan2 ⊢ W ∈ V ∧ φ → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
15 12 14 eqtrd ⊢ W ∈ V ∧ φ → A = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
16 15 fveq2d ⊢ W ∈ V ∧ φ → ⋅ A = ⋅ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
17 11 16 eqtr4id ⊢ W ∈ V ∧ φ → ⋅ W = ⋅ A
18 5 str0 ⊢ ∅ = ⋅ ∅
19 fvprc ⊢ ¬ W ∈ V → ⋅ W = ∅
20 19 adantr ⊢ ¬ W ∈ V ∧ φ → ⋅ W = ∅
21 fv2prc ⊢ ¬ W ∈ V → subringAlg ⁡ W ⁡ S = ∅
22 1 21 sylan9eqr ⊢ ¬ W ∈ V ∧ φ → A = ∅
23 22 fveq2d ⊢ ¬ W ∈ V ∧ φ → ⋅ A = ⋅ ∅
24 18 20 23 3eqtr4a ⊢ ¬ W ∈ V ∧ φ → ⋅ W = ⋅ A
25 17 24 pm2.61ian ⊢ φ → ⋅ W = ⋅ A