Metamath Proof Explorer

Theorem naddcnfass

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

Ref Expression
Assertion naddcnfass 
|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S /\ H e. S ) ) -> ( ( F oF +o G ) oF +o H ) = ( F oF +o ( G oF +o H ) ) )

Proof

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