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={\mathrm{Base}}_R$$
	srgfcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	srgfcl	$$⊢\left(R\in \mathrm{SRing}\wedge \underset{\dot{}}{·}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{·}:B\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		srgfcl.b	$$⊢B={\mathrm{Base}}_R$$
2		srgfcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		simpr	$$⊢\left(R\in \mathrm{SRing}\wedge \underset{\dot{}}{·}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{·}Fn\left(B\times B\right)$$
4	1 2	srgcl	$$⊢\left(R\in \mathrm{SRing}\wedge a\in B\wedge b\in B\right)\to a\underset{\dot{}}{·}b\in B$$
5	4	3expb	$$⊢\left(R\in \mathrm{SRing}\wedge \left(a\in B\wedge b\in B\right)\right)\to a\underset{\dot{}}{·}b\in B$$
6	5	ralrimivva	$$⊢R\in \mathrm{SRing}\to \forall a\in B\forall b\in Ba\underset{\dot{}}{·}b\in B$$
7		fveq2	$$⊢c=⟨a,b⟩\to \underset{\dot{}}{·}\left(c\right)=\underset{\dot{}}{·}\left(⟨a,b⟩\right)$$
8	7	eleq1d	$$⊢c=⟨a,b⟩\to \left(\underset{\dot{}}{·}\left(c\right)\in B\leftrightarrow \underset{\dot{}}{·}\left(⟨a,b⟩\right)\in B\right)$$
9		df-ov	$$⊢a\underset{\dot{}}{·}b=\underset{\dot{}}{·}\left(⟨a,b⟩\right)$$
10	9	eqcomi	$$⊢\underset{\dot{}}{·}\left(⟨a,b⟩\right)=a\underset{\dot{}}{·}b$$
11	10	eleq1i	$$⊢\underset{\dot{}}{·}\left(⟨a,b⟩\right)\in B\leftrightarrow a\underset{\dot{}}{·}b\in B$$
12	8 11	bitrdi	$$⊢c=⟨a,b⟩\to \left(\underset{\dot{}}{·}\left(c\right)\in B\leftrightarrow a\underset{\dot{}}{·}b\in B\right)$$
13	12	ralxp	$$⊢\forall c\in \left(B\times B\right)\underset{\dot{}}{·}\left(c\right)\in B\leftrightarrow \forall a\in B\forall b\in Ba\underset{\dot{}}{·}b\in B$$
14	6 13	sylibr	$$⊢R\in \mathrm{SRing}\to \forall c\in \left(B\times B\right)\underset{\dot{}}{·}\left(c\right)\in B$$
15	14	adantr	$$⊢\left(R\in \mathrm{SRing}\wedge \underset{\dot{}}{·}Fn\left(B\times B\right)\right)\to \forall c\in \left(B\times B\right)\underset{\dot{}}{·}\left(c\right)\in B$$
16		fnfvrnss	$$⊢\left(\underset{\dot{}}{·}Fn\left(B\times B\right)\wedge \forall c\in \left(B\times B\right)\underset{\dot{}}{·}\left(c\right)\in B\right)\to \mathrm{ran}\underset{\dot{}}{·}\subseteq B$$
17	3 15 16	syl2anc	$$⊢\left(R\in \mathrm{SRing}\wedge \underset{\dot{}}{·}Fn\left(B\times B\right)\right)\to \mathrm{ran}\underset{\dot{}}{·}\subseteq B$$
18		df-f	$$⊢\underset{\dot{}}{·}:B\times B⟶B\leftrightarrow \left(\underset{\dot{}}{·}Fn\left(B\times B\right)\wedge \mathrm{ran}\underset{\dot{}}{·}\subseteq B\right)$$
19	3 17 18	sylanbrc	$$⊢\left(R\in \mathrm{SRing}\wedge \underset{\dot{}}{·}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{·}:B\times B⟶B$$