Metamath Proof Explorer


Theorem srasca

Description: The set of scalars 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 srasca φ W 𝑠 S = Scalar A

Proof

Step Hyp Ref Expression
1 srapart.a φ A = subringAlg W S
2 srapart.s φ S Base W
3 scaid Scalar = Slot Scalar ndx
4 5re 5
5 5lt6 5 < 6
6 4 5 ltneii 5 6
7 scandx Scalar ndx = 5
8 vscandx ndx = 6
9 7 8 neeq12i Scalar ndx ndx 5 6
10 6 9 mpbir Scalar ndx ndx
11 3 10 setsnid Scalar W sSet Scalar ndx W 𝑠 S = Scalar W sSet Scalar ndx W 𝑠 S sSet ndx W
12 5lt8 5 < 8
13 4 12 ltneii 5 8
14 ipndx 𝑖 ndx = 8
15 7 14 neeq12i Scalar ndx 𝑖 ndx 5 8
16 13 15 mpbir Scalar ndx 𝑖 ndx
17 3 16 setsnid Scalar W sSet Scalar ndx W 𝑠 S sSet ndx W = Scalar W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W
18 11 17 eqtri Scalar W sSet Scalar ndx W 𝑠 S = Scalar W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W
19 ovexd φ W 𝑠 S V
20 3 setsid W V W 𝑠 S V W 𝑠 S = Scalar W sSet Scalar ndx W 𝑠 S
21 19 20 sylan2 W V φ W 𝑠 S = Scalar W sSet Scalar ndx W 𝑠 S
22 1 adantl W V φ A = subringAlg W S
23 sraval W V S Base W subringAlg W S = W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W
24 2 23 sylan2 W V φ subringAlg W S = W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W
25 22 24 eqtrd W V φ A = W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W
26 25 fveq2d W V φ Scalar A = Scalar W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W
27 18 21 26 3eqtr4a W V φ W 𝑠 S = Scalar A
28 3 str0 = Scalar
29 reldmress Rel dom 𝑠
30 29 ovprc1 ¬ W V W 𝑠 S =
31 30 adantr ¬ W V φ W 𝑠 S =
32 fv2prc ¬ W V subringAlg W S =
33 1 32 sylan9eqr ¬ W V φ A =
34 33 fveq2d ¬ W V φ Scalar A = Scalar
35 28 31 34 3eqtr4a ¬ W V φ W 𝑠 S = Scalar A
36 27 35 pm2.61ian φ W 𝑠 S = Scalar A