Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sravsca Structured version   Unicode version

Theorem sravsca 18348
 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.)
Hypotheses
Ref Expression
srapart.a subringAlg
srapart.s
Assertion
Ref Expression
sravsca

Proof of Theorem sravsca
StepHypRef Expression
1 srapart.a . . . . . 6 subringAlg
21adantl 467 . . . . 5 subringAlg
3 srapart.s . . . . . 6
4 sraval 18342 . . . . . 6 subringAlg sSet Scalar s sSet sSet
53, 4sylan2 476 . . . . 5 subringAlg sSet Scalar s sSet sSet
62, 5eqtrd 2462 . . . 4 sSet Scalar s sSet sSet
76fveq2d 5829 . . 3 sSet Scalar s sSet sSet
8 ovex 6277 . . . . 5 sSet Scalar s
9 fvex 5835 . . . . 5
10 vscaid 15203 . . . . . 6 Slot
1110setsid 15107 . . . . 5 sSet Scalar s sSet Scalar s sSet
128, 9, 11mp2an 676 . . . 4 sSet Scalar s sSet
13 6re 10641 . . . . . . 7
14 6lt8 10749 . . . . . . 7
1513, 14ltneii 9698 . . . . . 6
16 vscandx 15202 . . . . . . 7
17 ipndx 15209 . . . . . . 7
1816, 17neeq12i 2667 . . . . . 6
1915, 18mpbir 212 . . . . 5
2010, 19setsnid 15108 . . . 4 sSet Scalar s sSet sSet Scalar s sSet sSet
2112, 20eqtri 2450 . . 3 sSet Scalar s sSet sSet
227, 21syl6reqr 2481 . 2
2310str0 15104 . . 3
24 fvprc 5819 . . . 4