Step |
Hyp |
Ref |
Expression |
1 |
|
srgfcl.b |
|- B = ( Base ` R ) |
2 |
|
srgfcl.t |
|- .x. = ( .r ` R ) |
3 |
|
simpr |
|- ( ( R e. SRing /\ .x. Fn ( B X. B ) ) -> .x. Fn ( B X. B ) ) |
4 |
1 2
|
srgcl |
|- ( ( R e. SRing /\ a e. B /\ b e. B ) -> ( a .x. b ) e. B ) |
5 |
4
|
3expb |
|- ( ( R e. SRing /\ ( a e. B /\ b e. B ) ) -> ( a .x. b ) e. B ) |
6 |
5
|
ralrimivva |
|- ( R e. SRing -> A. a e. B A. b e. B ( a .x. b ) e. B ) |
7 |
|
fveq2 |
|- ( c = <. a , b >. -> ( .x. ` c ) = ( .x. ` <. a , b >. ) ) |
8 |
7
|
eleq1d |
|- ( c = <. a , b >. -> ( ( .x. ` c ) e. B <-> ( .x. ` <. a , b >. ) e. B ) ) |
9 |
|
df-ov |
|- ( a .x. b ) = ( .x. ` <. a , b >. ) |
10 |
9
|
eqcomi |
|- ( .x. ` <. a , b >. ) = ( a .x. b ) |
11 |
10
|
eleq1i |
|- ( ( .x. ` <. a , b >. ) e. B <-> ( a .x. b ) e. B ) |
12 |
8 11
|
bitrdi |
|- ( c = <. a , b >. -> ( ( .x. ` c ) e. B <-> ( a .x. b ) e. B ) ) |
13 |
12
|
ralxp |
|- ( A. c e. ( B X. B ) ( .x. ` c ) e. B <-> A. a e. B A. b e. B ( a .x. b ) e. B ) |
14 |
6 13
|
sylibr |
|- ( R e. SRing -> A. c e. ( B X. B ) ( .x. ` c ) e. B ) |
15 |
14
|
adantr |
|- ( ( R e. SRing /\ .x. Fn ( B X. B ) ) -> A. c e. ( B X. B ) ( .x. ` c ) e. B ) |
16 |
|
fnfvrnss |
|- ( ( .x. Fn ( B X. B ) /\ A. c e. ( B X. B ) ( .x. ` c ) e. B ) -> ran .x. C_ B ) |
17 |
3 15 16
|
syl2anc |
|- ( ( R e. SRing /\ .x. Fn ( B X. B ) ) -> ran .x. C_ B ) |
18 |
|
df-f |
|- ( .x. : ( B X. B ) --> B <-> ( .x. Fn ( B X. B ) /\ ran .x. C_ B ) ) |
19 |
3 17 18
|
sylanbrc |
|- ( ( R e. SRing /\ .x. Fn ( B X. B ) ) -> .x. : ( B X. B ) --> B ) |