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 ) ) |