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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	srgfcl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	srgfcl	⊢ ( ( 𝑅 ∈ SRing ∧ · Fn ( 𝐵 × 𝐵 ) ) → · : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		srgfcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		srgfcl.t	⊢ · = ( .r ‘ 𝑅 )
3		simpr	⊢ ( ( 𝑅 ∈ SRing ∧ · Fn ( 𝐵 × 𝐵 ) ) → · Fn ( 𝐵 × 𝐵 ) )
4	1 2	srgcl	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
5	4	3expb	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
6	5	ralrimivva	⊢ ( 𝑅 ∈ SRing → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 · 𝑏 ) ∈ 𝐵 )
7		fveq2	⊢ ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ → ( · ‘ 𝑐 ) = ( · ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
8	7	eleq1d	⊢ ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( · ‘ 𝑐 ) ∈ 𝐵 ↔ ( · ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝐵 ) )
9		df-ov	⊢ ( 𝑎 · 𝑏 ) = ( · ‘ ⟨ 𝑎 , 𝑏 ⟩ )
10	9	eqcomi	⊢ ( · ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ( 𝑎 · 𝑏 )
11	10	eleq1i	⊢ ( ( · ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ∈ 𝐵 ↔ ( 𝑎 · 𝑏 ) ∈ 𝐵 )
12	8 11	bitrdi	⊢ ( 𝑐 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( · ‘ 𝑐 ) ∈ 𝐵 ↔ ( 𝑎 · 𝑏 ) ∈ 𝐵 ) )
13	12	ralxp	⊢ ( ∀ 𝑐 ∈ ( 𝐵 × 𝐵 ) ( · ‘ 𝑐 ) ∈ 𝐵 ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 · 𝑏 ) ∈ 𝐵 )
14	6 13	sylibr	⊢ ( 𝑅 ∈ SRing → ∀ 𝑐 ∈ ( 𝐵 × 𝐵 ) ( · ‘ 𝑐 ) ∈ 𝐵 )
15	14	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ · Fn ( 𝐵 × 𝐵 ) ) → ∀ 𝑐 ∈ ( 𝐵 × 𝐵 ) ( · ‘ 𝑐 ) ∈ 𝐵 )
16		fnfvrnss	⊢ ( ( · Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑐 ∈ ( 𝐵 × 𝐵 ) ( · ‘ 𝑐 ) ∈ 𝐵 ) → ran · ⊆ 𝐵 )
17	3 15 16	syl2anc	⊢ ( ( 𝑅 ∈ SRing ∧ · Fn ( 𝐵 × 𝐵 ) ) → ran · ⊆ 𝐵 )
18		df-f	⊢ ( · : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ ( · Fn ( 𝐵 × 𝐵 ) ∧ ran · ⊆ 𝐵 ) )
19	3 17 18	sylanbrc	⊢ ( ( 𝑅 ∈ SRing ∧ · Fn ( 𝐵 × 𝐵 ) ) → · : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )