Metamath Proof Explorer

Theorem sralem

Description: Lemma for srabase and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 29-Oct-2024)

Ref Expression
Hypotheses srapart.a 
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
srapart.s 
|- ( ph -> S C_ ( Base ` W ) )
sralem.1 
|- E = Slot ( E ` ndx )
sralem.2 
|- ( Scalar ` ndx ) =/= ( E ` ndx )
sralem.3 
|- ( .s ` ndx ) =/= ( E ` ndx )
sralem.4 
|- ( .i ` ndx ) =/= ( E ` ndx )
Assertion sralem 
|- ( ph -> ( E ` W ) = ( E ` A ) )

Proof

Step Hyp Ref Expression
1 srapart.a 
 |-  ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2 srapart.s 
 |-  ( ph -> S C_ ( Base ` W ) )
3 sralem.1 
 |-  E = Slot ( E ` ndx )
4 sralem.2 
 |-  ( Scalar ` ndx ) =/= ( E ` ndx )
5 sralem.3 
 |-  ( .s ` ndx ) =/= ( E ` ndx )
6 sralem.4 
 |-  ( .i ` ndx ) =/= ( E ` ndx )
7 4 necomi 
 |-  ( E ` ndx ) =/= ( Scalar ` ndx )
8 3 7 setsnid 
 |-  ( E ` W ) = ( E ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) )
9 5 necomi 
 |-  ( E ` ndx ) =/= ( .s ` ndx )
10 3 9 setsnid 
 |-  ( E ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) ) = ( E ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
11 6 necomi 
 |-  ( E ` ndx ) =/= ( .i ` ndx )
12 3 11 setsnid 
 |-  ( E ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) ) = ( E ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
13 8 10 12 3eqtri 
 |-  ( E ` W ) = ( E ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
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 ) -> ( E ` A ) = ( E ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) ) )
19 13 18 eqtr4id 
 |-  ( ( W e. _V /\ ph ) -> ( E ` W ) = ( E ` A ) )
20 3 str0 
 |-  (/) = ( E ` (/) )
21 fvprc 
 |-  ( -. W e. _V -> ( E ` W ) = (/) )
22 21 adantr 
 |-  ( ( -. W e. _V /\ ph ) -> ( E ` W ) = (/) )
23 fv2prc 
 |-  ( -. W e. _V -> ( ( subringAlg ` W ) ` S ) = (/) )
24 1 23 sylan9eqr 
 |-  ( ( -. W e. _V /\ ph ) -> A = (/) )
25 24 fveq2d 
 |-  ( ( -. W e. _V /\ ph ) -> ( E ` A ) = ( E ` (/) ) )
26 20 22 25 3eqtr4a 
 |-  ( ( -. W e. _V /\ ph ) -> ( E ` W ) = ( E ` A ) )
27 19 26 pm2.61ian 
 |-  ( ph -> ( E ` W ) = ( E ` A ) )