Metamath Proof Explorer


Theorem srgfcl

Description: Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by AV, 24-Aug-2021)

Ref Expression
Hypotheses srgfcl.b
|- B = ( Base ` R )
srgfcl.t
|- .x. = ( .r ` R )
Assertion srgfcl
|- ( ( R e. SRing /\ .x. Fn ( B X. B ) ) -> .x. : ( B X. B ) --> B )

Proof

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 )