naddcnfass

Description: Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025)

		Ref	Expression
	Assertion	naddcnfass	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to (F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H = F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (X \in On \land S = dom (ω CNF X)) \to S = dom (ω CNF X)$
2	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \leftrightarrow F \in dom (ω CNF X))$
3		eqid	$⊢ dom (ω CNF X) = dom (ω CNF X)$
4		omelon	$⊢ ω \in On$
5	4	a1i	$⊢ (X \in On \land S = dom (ω CNF X)) \to ω \in On$
6		simpl	$⊢ (X \in On \land S = dom (ω CNF X)) \to X \in On$
7	3 5 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in dom (ω CNF X) \leftrightarrow (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)))$
8	2 7	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \leftrightarrow (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)))$
9		simpl	$⊢ (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)) \to F : X ⟶ ω$
10	9	ffnd	$⊢ (F : X ⟶ ω \land {finSupp}_{\emptyset} (F)) \to F Fn X$
11	8 10	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \to F Fn X)$
12		simp1	$⊢ (F \in S \land G \in S \land H \in S) \to F \in S$
13	11 12	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to F Fn X$
14	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \leftrightarrow G \in dom (ω CNF X))$
15	3 5 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in dom (ω CNF X) \leftrightarrow (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)))$
16	14 15	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \leftrightarrow (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)))$
17		simpl	$⊢ (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)) \to G : X ⟶ ω$
18	17	ffnd	$⊢ (G : X ⟶ ω \land {finSupp}_{\emptyset} (G)) \to G Fn X$
19	16 18	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \to G Fn X)$
20		simp2	$⊢ (F \in S \land G \in S \land H \in S) \to G \in S$
21	19 20	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to G Fn X$
22	6	adantr	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to X \in On$
23		inidm	$⊢ X \cap X = X$
24	13 21 22 22 23	offn	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to (F {+_{𝑜}}_{f} G) Fn X$
25	1	eleq2d	$⊢ (X \in On \land S = dom (ω CNF X)) \to (H \in S \leftrightarrow H \in dom (ω CNF X))$
26	3 5 6	cantnfs	$⊢ (X \in On \land S = dom (ω CNF X)) \to (H \in dom (ω CNF X) \leftrightarrow (H : X ⟶ ω \land {finSupp}_{\emptyset} (H)))$
27	25 26	bitrd	$⊢ (X \in On \land S = dom (ω CNF X)) \to (H \in S \leftrightarrow (H : X ⟶ ω \land {finSupp}_{\emptyset} (H)))$
28		simpl	$⊢ (H : X ⟶ ω \land {finSupp}_{\emptyset} (H)) \to H : X ⟶ ω$
29	28	ffnd	$⊢ (H : X ⟶ ω \land {finSupp}_{\emptyset} (H)) \to H Fn X$
30	27 29	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (H \in S \to H Fn X)$
31		simp3	$⊢ (F \in S \land G \in S \land H \in S) \to H \in S$
32	30 31	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to H Fn X$
33	24 32 22 22 23	offn	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) Fn X$
34	21 32 22 22 23	offn	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to (G {+_{𝑜}}_{f} H) Fn X$
35	13 34 22 22 23	offn	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) Fn X$
36	8 9	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (F \in S \to F : X ⟶ ω)$
37	36 12	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to F : X ⟶ ω$
38	37	ffvelcdmda	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to F (x) \in ω$
39	16 17	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (G \in S \to G : X ⟶ ω)$
40	39 20	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to G : X ⟶ ω$
41	40	ffvelcdmda	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to G (x) \in ω$
42	27 28	syl6bi	$⊢ (X \in On \land S = dom (ω CNF X)) \to (H \in S \to H : X ⟶ ω)$
43	42 31	impel	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to H : X ⟶ ω$
44	43	ffvelcdmda	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to H (x) \in ω$
45		nnaass	$⊢ (F (x) \in ω \land G (x) \in ω \land H (x) \in ω) \to (F (x) +_{𝑜} G (x)) +_{𝑜} H (x) = F (x) +_{𝑜} (G (x) +_{𝑜} H (x))$
46	38 41 44 45	syl3anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (F (x) +_{𝑜} G (x)) +_{𝑜} H (x) = F (x) +_{𝑜} (G (x) +_{𝑜} H (x))$
47	13	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to F Fn X$
48	21	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to G Fn X$
49	22	anim1i	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (X \in On \land x \in X)$
50		fnfvof	$⊢ ((F Fn X \land G Fn X) \land (X \in On \land x \in X)) \to (F {+_{𝑜}}_{f} G) (x) = F (x) +_{𝑜} G (x)$
51	47 48 49 50	syl21anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} G) (x) = F (x) +_{𝑜} G (x)$
52	51	oveq1d	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} G) (x) +_{𝑜} H (x) = (F (x) +_{𝑜} G (x)) +_{𝑜} H (x)$
53	32	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to H Fn X$
54		fnfvof	$⊢ ((G Fn X \land H Fn X) \land (X \in On \land x \in X)) \to (G {+_{𝑜}}_{f} H) (x) = G (x) +_{𝑜} H (x)$
55	48 53 49 54	syl21anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (G {+_{𝑜}}_{f} H) (x) = G (x) +_{𝑜} H (x)$
56	55	oveq2d	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to F (x) +_{𝑜} (G {+_{𝑜}}_{f} H) (x) = F (x) +_{𝑜} (G (x) +_{𝑜} H (x))$
57	46 52 56	3eqtr4d	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} G) (x) +_{𝑜} H (x) = F (x) +_{𝑜} (G {+_{𝑜}}_{f} H) (x)$
58	24	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} G) Fn X$
59		fnfvof	$⊢ (((F {+_{𝑜}}_{f} G) Fn X \land H Fn X) \land (X \in On \land x \in X)) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) (x) = (F {+_{𝑜}}_{f} G) (x) +_{𝑜} H (x)$
60	58 53 49 59	syl21anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) (x) = (F {+_{𝑜}}_{f} G) (x) +_{𝑜} H (x)$
61	34	adantr	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (G {+_{𝑜}}_{f} H) Fn X$
62		fnfvof	$⊢ ((F Fn X \land (G {+_{𝑜}}_{f} H) Fn X) \land (X \in On \land x \in X)) \to (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) (x) = F (x) +_{𝑜} (G {+_{𝑜}}_{f} H) (x)$
63	47 61 49 62	syl21anc	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) (x) = F (x) +_{𝑜} (G {+_{𝑜}}_{f} H) (x)$
64	57 60 63	3eqtr4d	$⊢ (((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \land x \in X) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) (x) = (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) (x)$
65	33 35 64	eqfnfvd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S \land H \in S)) \to (F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H = F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)$

Metamath Proof Explorer

Theorem naddcnfass

Proof