Metamath Proof Explorer


Theorem algsca

Description: The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypothesis algpart.a โŠข ๐ด = ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , + โŸฉ , โŸจ ( .r โ€˜ ndx ) , ร— โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ยท โŸฉ } )
Assertion algsca ( ๐‘† โˆˆ ๐‘‰ โ†’ ๐‘† = ( Scalar โ€˜ ๐ด ) )

Proof

Step Hyp Ref Expression
1 algpart.a โŠข ๐ด = ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , + โŸฉ , โŸจ ( .r โ€˜ ndx ) , ร— โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ยท โŸฉ } )
2 1 algstr โŠข ๐ด Struct โŸจ 1 , 6 โŸฉ
3 scaid โŠข Scalar = Slot ( Scalar โ€˜ ndx )
4 snsspr1 โŠข { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ } โŠ† { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ยท โŸฉ }
5 ssun2 โŠข { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ยท โŸฉ } โŠ† ( { โŸจ ( Base โ€˜ ndx ) , ๐ต โŸฉ , โŸจ ( +g โ€˜ ndx ) , + โŸฉ , โŸจ ( .r โ€˜ ndx ) , ร— โŸฉ } โˆช { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ยท โŸฉ } )
6 5 1 sseqtrri โŠข { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ , โŸจ ( ยท๐‘  โ€˜ ndx ) , ยท โŸฉ } โŠ† ๐ด
7 4 6 sstri โŠข { โŸจ ( Scalar โ€˜ ndx ) , ๐‘† โŸฉ } โŠ† ๐ด
8 2 3 7 strfv โŠข ( ๐‘† โˆˆ ๐‘‰ โ†’ ๐‘† = ( Scalar โ€˜ ๐ด ) )