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)

Ref Expression
Hypotheses srapart.a 
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
srapart.s 
|- ( ph -> S C_ ( Base ` W ) )
sralem.1 
|- E = Slot N
sralem.2 
|- N e. NN
sralem.3 
|- ( N < 5 \/ 8 < N )
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 N
4 sralem.2 
 |-  N e. NN
5 sralem.3 
 |-  ( N < 5 \/ 8 < N )
6 3 4 ndxid 
 |-  E = Slot ( E ` ndx )
7 4 nnrei 
 |-  N e. RR
8 5re 
 |-  5 e. RR
9 7 8 ltnei 
 |-  ( N < 5 -> 5 =/= N )
10 9 necomd 
 |-  ( N < 5 -> N =/= 5 )
11 5lt8 
 |-  5 < 8
12 8re 
 |-  8 e. RR
13 8 12 7 lttri 
 |-  ( ( 5 < 8 /\ 8 < N ) -> 5 < N )
14 11 13 mpan 
 |-  ( 8 < N -> 5 < N )
15 8 7 ltnei 
 |-  ( 5 < N -> N =/= 5 )
16 14 15 syl 
 |-  ( 8 < N -> N =/= 5 )
17 10 16 jaoi 
 |-  ( ( N < 5 \/ 8 < N ) -> N =/= 5 )
18 5 17 ax-mp 
 |-  N =/= 5
19 3 4 ndxarg 
 |-  ( E ` ndx ) = N
20 scandx 
 |-  ( Scalar ` ndx ) = 5
21 19 20 neeq12i 
 |-  ( ( E ` ndx ) =/= ( Scalar ` ndx ) <-> N =/= 5 )
22 18 21 mpbir 
 |-  ( E ` ndx ) =/= ( Scalar ` ndx )
23 6 22 setsnid 
 |-  ( E ` W ) = ( E ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) )
24 5lt6 
 |-  5 < 6
25 6re 
 |-  6 e. RR
26 7 8 25 lttri 
 |-  ( ( N < 5 /\ 5 < 6 ) -> N < 6 )
27 24 26 mpan2 
 |-  ( N < 5 -> N < 6 )
28 7 25 ltnei 
 |-  ( N < 6 -> 6 =/= N )
29 27 28 syl 
 |-  ( N < 5 -> 6 =/= N )
30 29 necomd 
 |-  ( N < 5 -> N =/= 6 )
31 6lt8 
 |-  6 < 8
32 25 12 7 lttri 
 |-  ( ( 6 < 8 /\ 8 < N ) -> 6 < N )
33 31 32 mpan 
 |-  ( 8 < N -> 6 < N )
34 25 7 ltnei 
 |-  ( 6 < N -> N =/= 6 )
35 33 34 syl 
 |-  ( 8 < N -> N =/= 6 )
36 30 35 jaoi 
 |-  ( ( N < 5 \/ 8 < N ) -> N =/= 6 )
37 5 36 ax-mp 
 |-  N =/= 6
38 vscandx 
 |-  ( .s ` ndx ) = 6
39 19 38 neeq12i 
 |-  ( ( E ` ndx ) =/= ( .s ` ndx ) <-> N =/= 6 )
40 37 39 mpbir 
 |-  ( E ` ndx ) =/= ( .s ` ndx )
41 6 40 setsnid 
 |-  ( E ` ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) ) = ( E ` ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
42 7 8 12 lttri 
 |-  ( ( N < 5 /\ 5 < 8 ) -> N < 8 )
43 11 42 mpan2 
 |-  ( N < 5 -> N < 8 )
44 7 12 ltnei 
 |-  ( N < 8 -> 8 =/= N )
45 43 44 syl 
 |-  ( N < 5 -> 8 =/= N )
46 45 necomd 
 |-  ( N < 5 -> N =/= 8 )
47 12 7 ltnei 
 |-  ( 8 < N -> N =/= 8 )
48 46 47 jaoi 
 |-  ( ( N < 5 \/ 8 < N ) -> N =/= 8 )
49 5 48 ax-mp 
 |-  N =/= 8
50 ipndx 
 |-  ( .i ` ndx ) = 8
51 19 50 neeq12i 
 |-  ( ( E ` ndx ) =/= ( .i ` ndx ) <-> N =/= 8 )
52 49 51 mpbir 
 |-  ( E ` ndx ) =/= ( .i ` ndx )
53 6 52 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 ) >. ) )
54 23 41 53 3eqtri 
 |-  ( E ` W ) = ( E ` ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
55 1 adantl 
 |-  ( ( W e. _V /\ ph ) -> A = ( ( subringAlg ` W ) ` S ) )
56 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 ) >. ) )
57 2 56 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 ) >. ) )
58 55 57 eqtrd 
 |-  ( ( W e. _V /\ ph ) -> A = ( ( ( W sSet <. ( Scalar ` ndx ) , ( W |`s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
59 58 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 ) >. ) ) )
60 54 59 eqtr4id 
 |-  ( ( W e. _V /\ ph ) -> ( E ` W ) = ( E ` A ) )
61 3 str0 
 |-  (/) = ( E ` (/) )
62 fvprc 
 |-  ( -. W e. _V -> ( E ` W ) = (/) )
63 62 adantr 
 |-  ( ( -. W e. _V /\ ph ) -> ( E ` W ) = (/) )
64 fv2prc 
 |-  ( -. W e. _V -> ( ( subringAlg ` W ) ` S ) = (/) )
65 1 64 sylan9eqr 
 |-  ( ( -. W e. _V /\ ph ) -> A = (/) )
66 65 fveq2d 
 |-  ( ( -. W e. _V /\ ph ) -> ( E ` A ) = ( E ` (/) ) )
67 61 63 66 3eqtr4a 
 |-  ( ( -. W e. _V /\ ph ) -> ( E ` W ) = ( E ` A ) )
68 60 67 pm2.61ian 
 |-  ( ph -> ( E ` W ) = ( E ` A ) )