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⊆BaseW
Assertion sravsca ⊢φ→⋅W=⋅A

Proof

Step Hyp Ref Expression
1 srapart.a ⊢φ→A=subringAlg⁡W⁡S
2 srapart.s ⊢φ→S⊆BaseW
3 ovex ⊢WsSetScalar⁡ndxW↾𝑠S∈V
4 fvex ⊢⋅W∈V
5 vscaid ⊢⋅𝑠=Slot⋅ndx
6 5 setsid ⊢WsSetScalar⁡ndxW↾𝑠S∈V∧⋅W∈V→⋅W=⋅WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅W
7 3 4 6 mp2an ⊢⋅W=⋅WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅W
8 slotsdifipndx ⊢⋅ndx≠⋅𝑖⁡ndx∧Scalar⁡ndx≠⋅𝑖⁡ndx
9 8 simpli ⊢⋅ndx≠⋅𝑖⁡ndx
10 5 9 setsnid ⊢⋅WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅W=⋅WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
11 7 10 eqtri ⊢⋅W=⋅WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
12 1 adantl ⊢W∈V∧φ→A=subringAlg⁡W⁡S
13 sraval ⊢W∈V∧S⊆BaseW→subringAlg⁡W⁡S=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
14 2 13 sylan2 ⊢W∈V∧φ→subringAlg⁡W⁡S=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
15 12 14 eqtrd ⊢W∈V∧φ→A=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
16 15 fveq2d ⊢W∈V∧φ→⋅A=⋅WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡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