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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	srgfcl	$⊢ (R \in SRing \land \underset{˙}{\cdot} Fn (B \times B)) \to \underset{˙}{\cdot} : B \times B ⟶ B$

Proof

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