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
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
srapart.s
|- ( ph -> S C_ ( Base ` W ) )
Assertion srasca
|- ( ph -> ( W |`s S ) = ( Scalar ` A ) )

Proof

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