Step |
Hyp |
Ref |
Expression |
1 |
|
i1fmulc.2 |
|- ( ph -> F e. dom S.1 ) |
2 |
|
i1fmulc.3 |
|- ( ph -> A e. RR ) |
3 |
|
reex |
|- RR e. _V |
4 |
3
|
a1i |
|- ( ph -> RR e. _V ) |
5 |
|
i1ff |
|- ( F e. dom S.1 -> F : RR --> RR ) |
6 |
1 5
|
syl |
|- ( ph -> F : RR --> RR ) |
7 |
6
|
ffnd |
|- ( ph -> F Fn RR ) |
8 |
|
eqidd |
|- ( ( ph /\ z e. RR ) -> ( F ` z ) = ( F ` z ) ) |
9 |
4 2 7 8
|
ofc1 |
|- ( ( ph /\ z e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` z ) = ( A x. ( F ` z ) ) ) |
10 |
9
|
ad4ant14 |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` z ) = ( A x. ( F ` z ) ) ) |
11 |
10
|
eqeq1d |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` z ) = B <-> ( A x. ( F ` z ) ) = B ) ) |
12 |
|
eqcom |
|- ( ( F ` z ) = ( B / A ) <-> ( B / A ) = ( F ` z ) ) |
13 |
|
simplr |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> B e. RR ) |
14 |
13
|
recnd |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> B e. CC ) |
15 |
2
|
ad3antrrr |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> A e. RR ) |
16 |
15
|
recnd |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> A e. CC ) |
17 |
6
|
ad2antrr |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> F : RR --> RR ) |
18 |
17
|
ffvelrnda |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( F ` z ) e. RR ) |
19 |
18
|
recnd |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( F ` z ) e. CC ) |
20 |
|
simpllr |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> A =/= 0 ) |
21 |
14 16 19 20
|
divmuld |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( B / A ) = ( F ` z ) <-> ( A x. ( F ` z ) ) = B ) ) |
22 |
12 21
|
syl5bb |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( F ` z ) = ( B / A ) <-> ( A x. ( F ` z ) ) = B ) ) |
23 |
11 22
|
bitr4d |
|- ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` z ) = B <-> ( F ` z ) = ( B / A ) ) ) |
24 |
23
|
pm5.32da |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( ( z e. RR /\ ( ( ( RR X. { A } ) oF x. F ) ` z ) = B ) <-> ( z e. RR /\ ( F ` z ) = ( B / A ) ) ) ) |
25 |
|
remulcl |
|- ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR ) |
26 |
25
|
adantl |
|- ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR ) |
27 |
|
fconstg |
|- ( A e. RR -> ( RR X. { A } ) : RR --> { A } ) |
28 |
2 27
|
syl |
|- ( ph -> ( RR X. { A } ) : RR --> { A } ) |
29 |
2
|
snssd |
|- ( ph -> { A } C_ RR ) |
30 |
28 29
|
fssd |
|- ( ph -> ( RR X. { A } ) : RR --> RR ) |
31 |
|
inidm |
|- ( RR i^i RR ) = RR |
32 |
26 30 6 4 4 31
|
off |
|- ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> RR ) |
33 |
32
|
ad2antrr |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( ( RR X. { A } ) oF x. F ) : RR --> RR ) |
34 |
33
|
ffnd |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( ( RR X. { A } ) oF x. F ) Fn RR ) |
35 |
|
fniniseg |
|- ( ( ( RR X. { A } ) oF x. F ) Fn RR -> ( z e. ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) <-> ( z e. RR /\ ( ( ( RR X. { A } ) oF x. F ) ` z ) = B ) ) ) |
36 |
34 35
|
syl |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( z e. ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) <-> ( z e. RR /\ ( ( ( RR X. { A } ) oF x. F ) ` z ) = B ) ) ) |
37 |
17
|
ffnd |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> F Fn RR ) |
38 |
|
fniniseg |
|- ( F Fn RR -> ( z e. ( `' F " { ( B / A ) } ) <-> ( z e. RR /\ ( F ` z ) = ( B / A ) ) ) ) |
39 |
37 38
|
syl |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( z e. ( `' F " { ( B / A ) } ) <-> ( z e. RR /\ ( F ` z ) = ( B / A ) ) ) ) |
40 |
24 36 39
|
3bitr4d |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( z e. ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) <-> z e. ( `' F " { ( B / A ) } ) ) ) |
41 |
40
|
eqrdv |
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) = ( `' F " { ( B / A ) } ) ) |