Metamath Proof Explorer

Theorem sraip

Description: The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses srapart.a ⊢φ→A=subringAlg⁡W⁡S
srapart.s ⊢φ→S⊆BaseW
Assertion sraip ⊢φ→⋅W=⋅𝑖⁡A

Proof

Step Hyp Ref Expression
1 srapart.a ⊢φ→A=subringAlg⁡W⁡S
2 srapart.s ⊢φ→S⊆BaseW
3 ovex ⊢WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅W∈V
4 fvex ⊢⋅W∈V
5 ipid ⊢⋅𝑖=Slot⋅𝑖⁡ndx
6 5 setsid ⊢WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅W∈V∧⋅W∈V→⋅W=⋅𝑖⁡WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
7 3 4 6 mp2an ⊢⋅W=⋅𝑖⁡WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
8 1 adantl ⊢W∈V∧φ→A=subringAlg⁡W⁡S
9 sraval ⊢W∈V∧S⊆BaseW→subringAlg⁡W⁡S=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
10 2 9 sylan2 ⊢W∈V∧φ→subringAlg⁡W⁡S=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
11 8 10 eqtrd ⊢W∈V∧φ→A=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
12 11 fveq2d ⊢W∈V∧φ→⋅𝑖⁡A=⋅𝑖⁡WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W
13 7 12 eqtr4id ⊢W∈V∧φ→⋅W=⋅𝑖⁡A
14 5 str0 ⊢∅=⋅𝑖⁡∅
15 fvprc ⊢¬W∈V→⋅W=∅
16 15 adantr ⊢¬W∈V∧φ→⋅W=∅
17 fv2prc ⊢¬W∈V→subringAlg⁡W⁡S=∅
18 1 17 sylan9eqr ⊢¬W∈V∧φ→A=∅
19 18 fveq2d ⊢¬W∈V∧φ→⋅𝑖⁡A=⋅𝑖⁡∅
20 14 16 19 3eqtr4a ⊢¬W∈V∧φ→⋅W=⋅𝑖⁡A
21 13 20 pm2.61ian ⊢φ→⋅W=⋅𝑖⁡A