Theorem plusfreseq

Description: If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020)

	Ref	Expression
Hypotheses	plusfreseq.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
	plusfreseq.2	⊢ + = ( +g ‘ 𝑀 )
	plusfreseq.3	⊢ ⨣ = ( +𝑓 ‘ 𝑀 )
Assertion	plusfreseq	⊢ ( ∅ ∉ ran ⨣ → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ )

Proof

Step	Hyp	Ref	Expression
1		plusfreseq.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		plusfreseq.2	⊢ + = ( +g ‘ 𝑀 )
3		plusfreseq.3	⊢ ⨣ = ( +𝑓 ‘ 𝑀 )
4	1 3	plusffn	⊢ ⨣ Fn ( 𝐵 × 𝐵 )
5		fnfun	⊢ ( ⨣ Fn ( 𝐵 × 𝐵 ) → Fun ⨣ )
6	4 5	ax-mp	⊢ Fun ⨣
7	6	a1i	⊢ ( ∅ ∉ ran ⨣ → Fun ⨣ )
8		id	⊢ ( ∅ ∉ ran ⨣ → ∅ ∉ ran ⨣ )
9	1 2 3	plusfval	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ⨣ 𝑦 ) = ( 𝑥 + 𝑦 ) )
10	9	eqcomd	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ⨣ 𝑦 ) )
11	10	rgen2	⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑥 ⨣ 𝑦 )
12	11	a1i	⊢ ( ∅ ∉ ran ⨣ → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑥 ⨣ 𝑦 ) )
13		fveq2	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( + ‘ 𝑝 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14		df-ov	⊢ ( 𝑥 + 𝑦 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ )
15	13 14	eqtr4di	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( + ‘ 𝑝 ) = ( 𝑥 + 𝑦 ) )
16		fveq2	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⨣ ‘ 𝑝 ) = ( ⨣ ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
17		df-ov	⊢ ( 𝑥 ⨣ 𝑦 ) = ( ⨣ ‘ ⟨ 𝑥 , 𝑦 ⟩ )
18	16 17	eqtr4di	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⨣ ‘ 𝑝 ) = ( 𝑥 ⨣ 𝑦 ) )
19	15 18	eqeq12d	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( + ‘ 𝑝 ) = ( ⨣ ‘ 𝑝 ) ↔ ( 𝑥 + 𝑦 ) = ( 𝑥 ⨣ 𝑦 ) ) )
20	19	ralxp	⊢ ( ∀ 𝑝 ∈ ( 𝐵 × 𝐵 ) ( + ‘ 𝑝 ) = ( ⨣ ‘ 𝑝 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑥 ⨣ 𝑦 ) )
21	12 20	sylibr	⊢ ( ∅ ∉ ran ⨣ → ∀ 𝑝 ∈ ( 𝐵 × 𝐵 ) ( + ‘ 𝑝 ) = ( ⨣ ‘ 𝑝 ) )
22		fndm	⊢ ( ⨣ Fn ( 𝐵 × 𝐵 ) → dom ⨣ = ( 𝐵 × 𝐵 ) )
23	22	eqcomd	⊢ ( ⨣ Fn ( 𝐵 × 𝐵 ) → ( 𝐵 × 𝐵 ) = dom ⨣ )
24	4 23	ax-mp	⊢ ( 𝐵 × 𝐵 ) = dom ⨣
25	24	fveqressseq	⊢ ( ( Fun ⨣ ∧ ∅ ∉ ran ⨣ ∧ ∀ 𝑝 ∈ ( 𝐵 × 𝐵 ) ( + ‘ 𝑝 ) = ( ⨣ ‘ 𝑝 ) ) → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ )
26	7 8 21 25	syl3anc	⊢ ( ∅ ∉ ran ⨣ → ( + ↾ ( 𝐵 × 𝐵 ) ) = ⨣ )