This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 ( 𝐵 × 𝐵 ) ) → · : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )