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 )