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) (Proof shortened by AV, 12-Nov-2024)

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 vscandxnscandx 
 |-  ( .s ` ndx ) =/= ( Scalar ` ndx )
5 4 necomi 
 |-  ( Scalar ` ndx ) =/= ( .s ` ndx )
6 3 5 setsnid 
 |-  ( Scalar ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) ) = ( Scalar ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
7 slotsdifipndx 
 |-  ( ( .s ` ndx ) =/= ( .i ` ndx ) /\ ( Scalar ` ndx ) =/= ( .i ` ndx ) )
8 7 simpri 
 |-  ( Scalar ` ndx ) =/= ( .i ` ndx )
9 3 8 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 ) >. ) )
10 6 9 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 ) >. ) )
11 ovexd 
 |-  ( ph -> ( W |`s S ) e. _V )
12 3 setsid 
 |-  ( ( W e. _V /\ ( W |`s S ) e. _V ) -> ( W |`s S ) = ( Scalar ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) ) )
13 11 12 sylan2 
 |-  ( ( W e. _V /\ ph ) -> ( W |`s S ) = ( Scalar ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) ) )
14 1 adantl 
 |-  ( ( W e. _V /\ ph ) -> A = ( ( subringAlg ` W ) ` S ) )
15 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 ) >. ) )
16 2 15 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 ) >. ) )
17 14 16 eqtrd 
 |-  ( ( W e. _V /\ ph ) -> A = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
18 17 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 ) >. ) ) )
19 10 13 18 3eqtr4a 
 |-  ( ( W e. _V /\ ph ) -> ( W |`s S ) = ( Scalar ` A ) )
20 3 str0 
 |-  (/) = ( Scalar ` (/) )
21 reldmress 
 |-  Rel dom |`s
22 21 ovprc1 
 |-  ( -. W e. _V -> ( W |`s S ) = (/) )
23 22 adantr 
 |-  ( ( -. W e. _V /\ ph ) -> ( W |`s S ) = (/) )
24 fv2prc 
 |-  ( -. W e. _V -> ( ( subringAlg ` W ) ` S ) = (/) )
25 1 24 sylan9eqr 
 |-  ( ( -. W e. _V /\ ph ) -> A = (/) )
26 25 fveq2d 
 |-  ( ( -. W e. _V /\ ph ) -> ( Scalar ` A ) = ( Scalar ` (/) ) )
27 20 23 26 3eqtr4a 
 |-  ( ( -. W e. _V /\ ph ) -> ( W |`s S ) = ( Scalar ` A ) )
28 19 27 pm2.61ian 
 |-  ( ph -> ( W |`s S ) = ( Scalar ` A ) )