Metamath Proof Explorer

Theorem cantnfval

Description: The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfcl.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cantnfcl.f 
|- ( ph -> F e. S )
cantnfval.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
Assertion cantnfval 
|- ( ph -> ( ( A CNF B ) ` F ) = ( H ` dom G ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 cantnfcl.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
5 cantnfcl.f 
 |-  ( ph -> F e. S )
6 cantnfval.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
7 eqid 
 |-  { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) }
8 7 2 3 cantnffval 
 |-  ( ph -> ( A CNF B ) = ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
9 8 fveq1d 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) ` F ) )
10 7 2 3 cantnfdm 
 |-  ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
11 1 10 eqtrid 
 |-  ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
12 5 11 eleqtrd 
 |-  ( ph -> F e. { g e. ( A ^m B ) | g finSupp (/) } )
13 ovex 
 |-  ( f supp (/) ) e. _V
14 eqid 
 |-  OrdIso ( _E , ( f supp (/) ) ) = OrdIso ( _E , ( f supp (/) ) )
15 14 oiexg 
 |-  ( ( f supp (/) ) e. _V -> OrdIso ( _E , ( f supp (/) ) ) e. _V )
16 13 15 mp1i 
 |-  ( f = F -> OrdIso ( _E , ( f supp (/) ) ) e. _V )
17 simpr 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> h = OrdIso ( _E , ( f supp (/) ) ) )
18 oveq1 
 |-  ( f = F -> ( f supp (/) ) = ( F supp (/) ) )
19 18 adantr 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( f supp (/) ) = ( F supp (/) ) )
20 oieq2 
 |-  ( ( f supp (/) ) = ( F supp (/) ) -> OrdIso ( _E , ( f supp (/) ) ) = OrdIso ( _E , ( F supp (/) ) ) )
21 19 20 syl 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> OrdIso ( _E , ( f supp (/) ) ) = OrdIso ( _E , ( F supp (/) ) ) )
22 17 21 eqtrd 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> h = OrdIso ( _E , ( F supp (/) ) ) )
23 22 4 eqtr4di 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> h = G )
24 23 fveq1d 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( h ` k ) = ( G ` k ) )
25 24 oveq2d 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( A ^o ( h ` k ) ) = ( A ^o ( G ` k ) ) )
26 simpl 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> f = F )
27 26 24 fveq12d 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( f ` ( h ` k ) ) = ( F ` ( G ` k ) ) )
28 25 27 oveq12d 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) = ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) )
29 28 oveq1d 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) = ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) )
30 29 mpoeq3dv 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) )
31 eqid 
 |-  (/) = (/)
32 seqomeq12 
 |-  ( ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) /\ (/) = (/) ) -> seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) ) )
33 30 31 32 sylancl 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) ) )
34 33 6 eqtr4di 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) = H )
35 23 dmeqd 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> dom h = dom G )
36 34 35 fveq12d 
 |-  ( ( f = F /\ h = OrdIso ( _E , ( f supp (/) ) ) ) -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) = ( H ` dom G ) )
37 16 36 csbied 
 |-  ( f = F -> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) = ( H ` dom G ) )
38 eqid 
 |-  ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) = ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) )
39 fvex 
 |-  ( H ` dom G ) e. _V
40 37 38 39 fvmpt 
 |-  ( F e. { g e. ( A ^m B ) | g finSupp (/) } -> ( ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) ` F ) = ( H ` dom G ) )
41 12 40 syl 
 |-  ( ph -> ( ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) ` F ) = ( H ` dom G ) )
42 9 41 eqtrd 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( H ` dom G ) )