ofoacom

Description: Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025)

		Ref	Expression
	Assertion	ofoacom	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to F {+_{𝑜}}_{f} G = G {+_{𝑜}}_{f} F$

Proof

Step	Hyp	Ref	Expression
1		elmapfn	$⊢ F \in (ω^{A}) \to F Fn A$
2	1	ad2antrl	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to F Fn A$
3		elmapfn	$⊢ G \in (ω^{A}) \to G Fn A$
4	3	ad2antll	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to G Fn A$
5		simpl	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to A \in V$
6		inidm	$⊢ A \cap A = A$
7	2 4 5 5 6	offn	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to (F {+_{𝑜}}_{f} G) Fn A$
8	4 2 5 5 6	offn	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to (G {+_{𝑜}}_{f} F) Fn A$
9		elmapi	$⊢ F \in (ω^{A}) \to F : A ⟶ ω$
10	9	ad2antrl	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to F : A ⟶ ω$
11	10	ffvelcdmda	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to F (a) \in ω$
12		elmapi	$⊢ G \in (ω^{A}) \to G : A ⟶ ω$
13	12	ad2antll	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to G : A ⟶ ω$
14	13	ffvelcdmda	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to G (a) \in ω$
15		nnacom	$⊢ (F (a) \in ω \land G (a) \in ω) \to F (a) +_{𝑜} G (a) = G (a) +_{𝑜} F (a)$
16	11 14 15	syl2anc	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to F (a) +_{𝑜} G (a) = G (a) +_{𝑜} F (a)$
17	2 4	jca	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to (F Fn A \land G Fn A)$
18	5	anim1i	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to (A \in V \land a \in A)$
19		fnfvof	$⊢ ((F Fn A \land G Fn A) \land (A \in V \land a \in A)) \to (F {+_{𝑜}}_{f} G) (a) = F (a) +_{𝑜} G (a)$
20	17 18 19	syl2an2r	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to (F {+_{𝑜}}_{f} G) (a) = F (a) +_{𝑜} G (a)$
21	4 2	jca	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to (G Fn A \land F Fn A)$
22		fnfvof	$⊢ ((G Fn A \land F Fn A) \land (A \in V \land a \in A)) \to (G {+_{𝑜}}_{f} F) (a) = G (a) +_{𝑜} F (a)$
23	21 18 22	syl2an2r	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to (G {+_{𝑜}}_{f} F) (a) = G (a) +_{𝑜} F (a)$
24	16 20 23	3eqtr4d	$⊢ ((A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \land a \in A) \to (F {+_{𝑜}}_{f} G) (a) = (G {+_{𝑜}}_{f} F) (a)$
25	7 8 24	eqfnfvd	$⊢ (A \in V \land (F \in (ω^{A}) \land G \in (ω^{A}))) \to F {+_{𝑜}}_{f} G = G {+_{𝑜}}_{f} F$

Metamath Proof Explorer

Theorem ofoacom

Proof