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

Theorem sravsca 16254
 Description: The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
Hypotheses
Ref Expression
srapart.a subringAlg
srapart.s
Assertion
Ref Expression
sravsca

Proof of Theorem sravsca
StepHypRef Expression
1 srapart.a . . . . . 6 subringAlg
21adantl 453 . . . . 5 subringAlg
3 srapart.s . . . . . 6
4 sraval 16248 . . . . . 6 subringAlg sSet Scalar s sSet
53, 4sylan2 461 . . . . 5 subringAlg sSet Scalar s sSet
62, 5eqtrd 2468 . . . 4 sSet Scalar s sSet
76fveq2d 5732 . . 3 sSet Scalar s sSet
8 ovex 6106 . . . 4 sSet Scalar s
9 fvex 5742 . . . 4
10 vscaid 13592 . . . . 5 Slot
1110setsid 13508 . . . 4 sSet Scalar s sSet Scalar s sSet
128, 9, 11mp2an 654 . . 3 sSet Scalar s sSet
137, 12syl6reqr 2487 . 2
1410str0 13505 . . 3
15 fvprc 5722 . . . 4