Metamath Proof Explorer

Theorem selvply1rhmlemb

Description: Lemma for selvply1rhm . (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses selvply1rhmlema.1 
|- B = ( Base ` P )
selvply1rhmlema.2 
|- P = ( { X } mPoly R )
selvply1rhmlema.3 
|- .x. = ( .r ` P )
selvply1rhmlema.4 
|- .X. = ( .r ` Q )
selvply1rhmlema.5 
|- Q = ( Poly1 ` R )
selvply1rhmlema.6 
|- M = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) )
selvply1rhmlema.7 
|- ( ph -> X e. V )
selvply1rhmlema.8 
|- ( ph -> R e. Ring )
selvply1rhmlema.9 
|- ( ph -> F e. B )
selvply1rhmlemb.10 
|- ( ph -> G e. B )
Assertion selvply1rhmlemb 
|- ( ph -> ( M ` ( F .x. G ) ) = ( ( M ` F ) .X. ( M ` G ) ) )

Proof

Step Hyp Ref Expression
1 selvply1rhmlema.1 
 |-  B = ( Base ` P )
2 selvply1rhmlema.2 
 |-  P = ( { X } mPoly R )
3 selvply1rhmlema.3 
 |-  .x. = ( .r ` P )
4 selvply1rhmlema.4 
 |-  .X. = ( .r ` Q )
5 selvply1rhmlema.5 
 |-  Q = ( Poly1 ` R )
6 selvply1rhmlema.6 
 |-  M = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) )
7 selvply1rhmlema.7 
 |-  ( ph -> X e. V )
8 selvply1rhmlema.8 
 |-  ( ph -> R e. Ring )
9 selvply1rhmlema.9 
 |-  ( ph -> F e. B )
10 selvply1rhmlemb.10 
 |-  ( ph -> G e. B )
11 fveq1 
 |-  ( f = ( F .x. G ) -> ( f ` { <. X , ( n ` (/) ) >. } ) = ( ( F .x. G ) ` { <. X , ( n ` (/) ) >. } ) )
12 11 mpteq2dv 
 |-  ( f = ( F .x. G ) -> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( F .x. G ) ` { <. X , ( n ` (/) ) >. } ) ) )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 eqid 
 |-  { g e. ( NN0 ^m { X } ) | g finSupp 0 } = { g e. ( NN0 ^m { X } ) | g finSupp 0 }
15 14 psrbasfsupp 
 |-  { g e. ( NN0 ^m { X } ) | g finSupp 0 } = { g e. ( NN0 ^m { X } ) | ( `' g " NN ) e. Fin }
16 2 1 13 3 15 9 10 mplmul 
 |-  ( ph -> ( F .x. G ) = ( m e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } |-> ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ m } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( m oF - j ) ) ) ) ) ) )
17 16 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( F .x. G ) = ( m e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } |-> ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ m } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( m oF - j ) ) ) ) ) ) )
18 breq2 
 |-  ( m = { <. X , ( n ` (/) ) >. } -> ( l oR <_ m <-> l oR <_ { <. X , ( n ` (/) ) >. } ) )
19 18 rabbidv 
 |-  ( m = { <. X , ( n ` (/) ) >. } -> { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ m } = { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } )
20 fvoveq1 
 |-  ( m = { <. X , ( n ` (/) ) >. } -> ( G ` ( m oF - j ) ) = ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) )
21 20 oveq2d 
 |-  ( m = { <. X , ( n ` (/) ) >. } -> ( ( F ` j ) ( .r ` R ) ( G ` ( m oF - j ) ) ) = ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) )
22 19 21 mpteq12dv 
 |-  ( m = { <. X , ( n ` (/) ) >. } -> ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ m } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( m oF - j ) ) ) ) = ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) ) )
23 22 oveq2d 
 |-  ( m = { <. X , ( n ` (/) ) >. } -> ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ m } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( m oF - j ) ) ) ) ) = ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) ) ) )
24 nfcv 
 |-  F/_ j ( ( F ` { <. X , ( i ` (/) ) >. } ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
27 fveq2 
 |-  ( j = { <. X , ( i ` (/) ) >. } -> ( F ` j ) = ( F ` { <. X , ( i ` (/) ) >. } ) )
28 oveq2 
 |-  ( j = { <. X , ( i ` (/) ) >. } -> ( { <. X , ( n ` (/) ) >. } oF - j ) = ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) )
29 28 fveq2d 
 |-  ( j = { <. X , ( i ` (/) ) >. } -> ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) = ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) )
30 27 29 oveq12d 
 |-  ( j = { <. X , ( i ` (/) ) >. } -> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) = ( ( F ` { <. X , ( i ` (/) ) >. } ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) ) )
31 8 ringcmnd 
 |-  ( ph -> R e. CMnd )
32 31 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> R e. CMnd )
33 eqid 
 |-  { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } = { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } }
34 ovexd 
 |-  ( ph -> ( NN0 ^m { X } ) e. _V )
35 14 34 rabexd 
 |-  ( ph -> { g e. ( NN0 ^m { X } ) | g finSupp 0 } e. _V )
36 33 35 rabexd 
 |-  ( ph -> { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } e. _V )
37 36 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } e. _V )
38 fvexd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( 0g ` R ) e. _V )
39 35 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { g e. ( NN0 ^m { X } ) | g finSupp 0 } e. _V )
40 ssrab2 
 |-  { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } C_ { g e. ( NN0 ^m { X } ) | g finSupp 0 }
41 40 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } C_ { g e. ( NN0 ^m { X } ) | g finSupp 0 } )
42 2 25 1 15 10 mplelf 
 |-  ( ph -> G : { g e. ( NN0 ^m { X } ) | g finSupp 0 } --> ( Base ` R ) )
43 42 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> G : { g e. ( NN0 ^m { X } ) | g finSupp 0 } --> ( Base ` R ) )
44 breq1 
 |-  ( g = { <. X , ( n ` (/) ) >. } -> ( g finSupp 0 <-> { <. X , ( n ` (/) ) >. } finSupp 0 ) )
45 nn0ex 
 |-  NN0 e. _V
46 45 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> NN0 e. _V )
47 snex 
 |-  { X } e. _V
48 47 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { X } e. _V )
49 7 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> X e. V )
50 1oex 
 |-  1o e. _V
51 50 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 1o e. _V )
52 simpr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n e. ( NN0 ^m 1o ) )
53 51 46 52 elmaprd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> NN0 )
54 0lt1o 
 |-  (/) e. 1o
55 54 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
56 53 55 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) e. NN0 )
57 49 56 fsnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
58 46 48 57 elmapdd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
59 snfi 
 |-  { X } e. Fin
60 59 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { X } e. Fin )
61 c0ex 
 |-  0 e. _V
62 61 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 0 e. _V )
63 57 60 62 fdmfifsupp 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
64 44 58 63 elrabd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } )
65 64 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. X , ( n ` (/) ) >. } e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } )
66 47 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { X } e. _V )
67 45 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> NN0 e. _V )
68 ssrab2 
 |-  { g e. ( NN0 ^m { X } ) | g finSupp 0 } C_ ( NN0 ^m { X } )
69 40 68 sstri 
 |-  { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } C_ ( NN0 ^m { X } )
70 69 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } C_ ( NN0 ^m { X } ) )
71 70 sselda 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> j e. ( NN0 ^m { X } ) )
72 66 67 71 elmaprd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> j : { X } --> NN0 )
73 breq1 
 |-  ( l = j -> ( l oR <_ { <. X , ( n ` (/) ) >. } <-> j oR <_ { <. X , ( n ` (/) ) >. } ) )
74 simpr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } )
75 73 74 elrabrd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> j oR <_ { <. X , ( n ` (/) ) >. } )
76 15 psrbagcon 
 |-  ( ( { <. X , ( n ` (/) ) >. } e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } /\ j : { X } --> NN0 /\ j oR <_ { <. X , ( n ` (/) ) >. } ) -> ( ( { <. X , ( n ` (/) ) >. } oF - j ) e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } /\ ( { <. X , ( n ` (/) ) >. } oF - j ) oR <_ { <. X , ( n ` (/) ) >. } ) )
77 65 72 75 76 syl3anc 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( ( { <. X , ( n ` (/) ) >. } oF - j ) e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } /\ ( { <. X , ( n ` (/) ) >. } oF - j ) oR <_ { <. X , ( n ` (/) ) >. } ) )
78 77 simpld 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( { <. X , ( n ` (/) ) >. } oF - j ) e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } )
79 43 78 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) e. ( Base ` R ) )
80 2 25 1 15 9 mplelf 
 |-  ( ph -> F : { g e. ( NN0 ^m { X } ) | g finSupp 0 } --> ( Base ` R ) )
81 80 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> F : { g e. ( NN0 ^m { X } ) | g finSupp 0 } --> ( Base ` R ) )
82 2 1 26 9 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
83 82 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> F finSupp ( 0g ` R ) )
84 8 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ x e. ( Base ` R ) ) -> R e. Ring )
85 simpr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ x e. ( Base ` R ) ) -> x e. ( Base ` R ) )
86 25 13 26 84 85 ringlzd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ x e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) )
87 38 38 39 41 79 81 83 86 fisuppov1 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) ) finSupp ( 0g ` R ) )
88 ssidd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( Base ` R ) C_ ( Base ` R ) )
89 8 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> R e. Ring )
90 80 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> F : { g e. ( NN0 ^m { X } ) | g finSupp 0 } --> ( Base ` R ) )
91 41 sselda 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> j e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } )
92 90 91 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( F ` j ) e. ( Base ` R ) )
93 25 13 89 92 79 ringcld 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) e. ( Base ` R ) )
94 breq1 
 |-  ( l = { <. X , ( i ` (/) ) >. } -> ( l oR <_ { <. X , ( n ` (/) ) >. } <-> { <. X , ( i ` (/) ) >. } oR <_ { <. X , ( n ` (/) ) >. } ) )
95 breq1 
 |-  ( g = { <. X , ( i ` (/) ) >. } -> ( g finSupp 0 <-> { <. X , ( i ` (/) ) >. } finSupp 0 ) )
96 45 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> NN0 e. _V )
97 47 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { X } e. _V )
98 49 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> X e. V )
99 50 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> 1o e. _V )
100 ssrab2 
 |-  { k e. ( NN0 ^m 1o ) | k oR <_ n } C_ ( NN0 ^m 1o )
101 100 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { k e. ( NN0 ^m 1o ) | k oR <_ n } C_ ( NN0 ^m 1o ) )
102 101 sselda 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i e. ( NN0 ^m 1o ) )
103 99 96 102 elmaprd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i : 1o --> NN0 )
104 54 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> (/) e. 1o )
105 103 104 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( i ` (/) ) e. NN0 )
106 98 105 fsnd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } : { X } --> NN0 )
107 96 97 106 elmapdd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } e. ( NN0 ^m { X } ) )
108 59 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { X } e. Fin )
109 61 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> 0 e. _V )
110 106 108 109 fdmfifsupp 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } finSupp 0 )
111 95 107 110 elrabd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } )
112 simplr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> n e. ( NN0 ^m 1o ) )
113 breq1 
 |-  ( k = i -> ( k oR <_ n <-> i oR <_ n ) )
114 simpr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } )
115 113 114 elrabrd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i oR <_ n )
116 elmapfn 
 |-  ( i e. ( NN0 ^m 1o ) -> i Fn 1o )
117 116 adantl 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ i e. ( NN0 ^m 1o ) ) -> i Fn 1o )
118 elmapfn 
 |-  ( n e. ( NN0 ^m 1o ) -> n Fn 1o )
119 118 adantr 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ i e. ( NN0 ^m 1o ) ) -> n Fn 1o )
120 50 a1i 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ i e. ( NN0 ^m 1o ) ) -> 1o e. _V )
121 inidm 
 |-  ( 1o i^i 1o ) = 1o
122 eqidd 
 |-  ( ( ( n e. ( NN0 ^m 1o ) /\ i e. ( NN0 ^m 1o ) ) /\ (/) e. 1o ) -> ( i ` (/) ) = ( i ` (/) ) )
123 eqidd 
 |-  ( ( ( n e. ( NN0 ^m 1o ) /\ i e. ( NN0 ^m 1o ) ) /\ (/) e. 1o ) -> ( n ` (/) ) = ( n ` (/) ) )
124 117 119 120 120 121 122 123 ofrval 
 |-  ( ( ( n e. ( NN0 ^m 1o ) /\ i e. ( NN0 ^m 1o ) ) /\ i oR <_ n /\ (/) e. 1o ) -> ( i ` (/) ) <_ ( n ` (/) ) )
125 112 102 115 104 124 syl211anc 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( i ` (/) ) <_ ( n ` (/) ) )
126 125 ralrimivw 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> A. x e. { X } ( i ` (/) ) <_ ( n ` (/) ) )
127 106 ffnd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } Fn { X } )
128 57 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
129 128 ffnd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( n ` (/) ) >. } Fn { X } )
130 inidm 
 |-  ( { X } i^i { X } ) = { X }
131 simpr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> x e. { X } )
132 131 elsnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> x = X )
133 132 fveq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> ( { <. X , ( i ` (/) ) >. } ` x ) = ( { <. X , ( i ` (/) ) >. } ` X ) )
134 fvsng 
 |-  ( ( X e. V /\ ( i ` (/) ) e. NN0 ) -> ( { <. X , ( i ` (/) ) >. } ` X ) = ( i ` (/) ) )
135 98 105 134 syl2anc 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( { <. X , ( i ` (/) ) >. } ` X ) = ( i ` (/) ) )
136 135 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> ( { <. X , ( i ` (/) ) >. } ` X ) = ( i ` (/) ) )
137 133 136 eqtrd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> ( { <. X , ( i ` (/) ) >. } ` x ) = ( i ` (/) ) )
138 132 fveq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> ( { <. X , ( n ` (/) ) >. } ` x ) = ( { <. X , ( n ` (/) ) >. } ` X ) )
139 56 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( n ` (/) ) e. NN0 )
140 fvsng 
 |-  ( ( X e. V /\ ( n ` (/) ) e. NN0 ) -> ( { <. X , ( n ` (/) ) >. } ` X ) = ( n ` (/) ) )
141 98 139 140 syl2anc 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( { <. X , ( n ` (/) ) >. } ` X ) = ( n ` (/) ) )
142 141 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> ( { <. X , ( n ` (/) ) >. } ` X ) = ( n ` (/) ) )
143 138 142 eqtrd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ x e. { X } ) -> ( { <. X , ( n ` (/) ) >. } ` x ) = ( n ` (/) ) )
144 127 129 97 97 130 137 143 ofrfval 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( { <. X , ( i ` (/) ) >. } oR <_ { <. X , ( n ` (/) ) >. } <-> A. x e. { X } ( i ` (/) ) <_ ( n ` (/) ) ) )
145 126 144 mpbird 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } oR <_ { <. X , ( n ` (/) ) >. } )
146 94 111 145 elrabd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } )
147 breq1 
 |-  ( k = { <. (/) , ( j ` X ) >. } -> ( k oR <_ n <-> { <. (/) , ( j ` X ) >. } oR <_ n ) )
148 50 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> 1o e. _V )
149 df1o2 
 |-  1o = { (/) }
150 149 eqcomi 
 |-  { (/) } = 1o
151 150 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { (/) } = 1o )
152 0ex 
 |-  (/) e. _V
153 152 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> (/) e. _V )
154 snidg 
 |-  ( X e. V -> X e. { X } )
155 7 154 syl 
 |-  ( ph -> X e. { X } )
156 155 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> X e. { X } )
157 72 156 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( j ` X ) e. NN0 )
158 153 157 fsnd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. (/) , ( j ` X ) >. } : { (/) } --> NN0 )
159 151 158 feq2dd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. (/) , ( j ` X ) >. } : 1o --> NN0 )
160 67 148 159 elmapdd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. (/) , ( j ` X ) >. } e. ( NN0 ^m 1o ) )
161 simplr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> n e. ( NN0 ^m 1o ) )
162 49 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> X e. V )
163 161 162 jca 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( n e. ( NN0 ^m 1o ) /\ X e. V ) )
164 elmapfn 
 |-  ( j e. ( NN0 ^m { X } ) -> j Fn { X } )
165 164 adantr 
 |-  ( ( j e. ( NN0 ^m { X } ) /\ ( n e. ( NN0 ^m 1o ) /\ X e. V ) ) -> j Fn { X } )
166 simpr 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ X e. V ) -> X e. V )
167 elmapi 
 |-  ( n e. ( NN0 ^m 1o ) -> n : 1o --> NN0 )
168 54 a1i 
 |-  ( n e. ( NN0 ^m 1o ) -> (/) e. 1o )
169 167 168 ffvelcdmd 
 |-  ( n e. ( NN0 ^m 1o ) -> ( n ` (/) ) e. NN0 )
170 169 adantr 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ X e. V ) -> ( n ` (/) ) e. NN0 )
171 166 170 fsnd 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ X e. V ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
172 171 ffnd 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ X e. V ) -> { <. X , ( n ` (/) ) >. } Fn { X } )
173 172 adantl 
 |-  ( ( j e. ( NN0 ^m { X } ) /\ ( n e. ( NN0 ^m 1o ) /\ X e. V ) ) -> { <. X , ( n ` (/) ) >. } Fn { X } )
174 47 a1i 
 |-  ( ( j e. ( NN0 ^m { X } ) /\ ( n e. ( NN0 ^m 1o ) /\ X e. V ) ) -> { X } e. _V )
175 eqidd 
 |-  ( ( ( j e. ( NN0 ^m { X } ) /\ ( n e. ( NN0 ^m 1o ) /\ X e. V ) ) /\ X e. { X } ) -> ( j ` X ) = ( j ` X ) )
176 166 170 140 syl2anc 
 |-  ( ( n e. ( NN0 ^m 1o ) /\ X e. V ) -> ( { <. X , ( n ` (/) ) >. } ` X ) = ( n ` (/) ) )
177 176 ad2antlr 
 |-  ( ( ( j e. ( NN0 ^m { X } ) /\ ( n e. ( NN0 ^m 1o ) /\ X e. V ) ) /\ X e. { X } ) -> ( { <. X , ( n ` (/) ) >. } ` X ) = ( n ` (/) ) )
178 165 173 174 174 130 175 177 ofrval 
 |-  ( ( ( j e. ( NN0 ^m { X } ) /\ ( n e. ( NN0 ^m 1o ) /\ X e. V ) ) /\ j oR <_ { <. X , ( n ` (/) ) >. } /\ X e. { X } ) -> ( j ` X ) <_ ( n ` (/) ) )
179 71 163 75 156 178 syl211anc 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( j ` X ) <_ ( n ` (/) ) )
180 fveq2 
 |-  ( o = (/) -> ( n ` o ) = ( n ` (/) ) )
181 180 breq2d 
 |-  ( o = (/) -> ( ( j ` X ) <_ ( n ` o ) <-> ( j ` X ) <_ ( n ` (/) ) ) )
182 152 181 ralsn 
 |-  ( A. o e. { (/) } ( j ` X ) <_ ( n ` o ) <-> ( j ` X ) <_ ( n ` (/) ) )
183 179 182 sylibr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> A. o e. { (/) } ( j ` X ) <_ ( n ` o ) )
184 149 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> 1o = { (/) } )
185 183 184 raleqtrrdv 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> A. o e. 1o ( j ` X ) <_ ( n ` o ) )
186 159 ffnd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. (/) , ( j ` X ) >. } Fn 1o )
187 118 ad2antlr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> n Fn 1o )
188 elsni 
 |-  ( o e. { (/) } -> o = (/) )
189 188 149 eleq2s 
 |-  ( o e. 1o -> o = (/) )
190 189 adantl 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ o e. 1o ) -> o = (/) )
191 190 fveq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ o e. 1o ) -> ( { <. (/) , ( j ` X ) >. } ` o ) = ( { <. (/) , ( j ` X ) >. } ` (/) ) )
192 157 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ o e. 1o ) -> ( j ` X ) e. NN0 )
193 fvsng 
 |-  ( ( (/) e. _V /\ ( j ` X ) e. NN0 ) -> ( { <. (/) , ( j ` X ) >. } ` (/) ) = ( j ` X ) )
194 152 192 193 sylancr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ o e. 1o ) -> ( { <. (/) , ( j ` X ) >. } ` (/) ) = ( j ` X ) )
195 191 194 eqtrd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ o e. 1o ) -> ( { <. (/) , ( j ` X ) >. } ` o ) = ( j ` X ) )
196 eqidd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ o e. 1o ) -> ( n ` o ) = ( n ` o ) )
197 186 187 148 148 121 195 196 ofrfval 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> ( { <. (/) , ( j ` X ) >. } oR <_ n <-> A. o e. 1o ( j ` X ) <_ ( n ` o ) ) )
198 185 197 mpbird 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. (/) , ( j ` X ) >. } oR <_ n )
199 147 160 198 elrabd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> { <. (/) , ( j ` X ) >. } e. { k e. ( NN0 ^m 1o ) | k oR <_ n } )
200 eqcom 
 |-  ( ( j ` X ) = ( i ` (/) ) <-> ( i ` (/) ) = ( j ` X ) )
201 200 a1i 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( j ` X ) = ( i ` (/) ) <-> ( i ` (/) ) = ( j ` X ) ) )
202 135 adantlr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( { <. X , ( i ` (/) ) >. } ` X ) = ( i ` (/) ) )
203 202 eqeq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( j ` X ) = ( { <. X , ( i ` (/) ) >. } ` X ) <-> ( j ` X ) = ( i ` (/) ) ) )
204 157 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( j ` X ) e. NN0 )
205 152 204 193 sylancr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( { <. (/) , ( j ` X ) >. } ` (/) ) = ( j ` X ) )
206 205 eqeq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( i ` (/) ) = ( { <. (/) , ( j ` X ) >. } ` (/) ) <-> ( i ` (/) ) = ( j ` X ) ) )
207 201 203 206 3bitr4d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( j ` X ) = ( { <. X , ( i ` (/) ) >. } ` X ) <-> ( i ` (/) ) = ( { <. (/) , ( j ` X ) >. } ` (/) ) ) )
208 162 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> X e. V )
209 eqid 
 |-  { X } = { X }
210 72 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> j : { X } --> NN0 )
211 210 ffnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> j Fn { X } )
212 127 adantlr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. X , ( i ` (/) ) >. } Fn { X } )
213 208 209 211 212 fsneq 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( j = { <. X , ( i ` (/) ) >. } <-> ( j ` X ) = ( { <. X , ( i ` (/) ) >. } ` X ) ) )
214 152 a1i 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> (/) e. _V )
215 103 adantlr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i : 1o --> NN0 )
216 215 ffnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i Fn 1o )
217 186 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { <. (/) , ( j ` X ) >. } Fn 1o )
218 214 149 216 217 fsneq 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( i = { <. (/) , ( j ` X ) >. } <-> ( i ` (/) ) = ( { <. (/) , ( j ` X ) >. } ` (/) ) ) )
219 207 213 218 3bitr4d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( j = { <. X , ( i ` (/) ) >. } <-> i = { <. (/) , ( j ` X ) >. } ) )
220 199 219 reu6dv 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } ) -> E! i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } j = { <. X , ( i ` (/) ) >. } )
221 24 25 26 30 32 37 87 88 93 146 220 gsummptfsf1o 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) ) ) = ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( F ` { <. X , ( i ` (/) ) >. } ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) ) ) ) )
222 100 a1i 
 |-  ( ph -> { k e. ( NN0 ^m 1o ) | k oR <_ n } C_ ( NN0 ^m 1o ) )
223 222 sselda 
 |-  ( ( ph /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i e. ( NN0 ^m 1o ) )
224 fveq1 
 |-  ( n = i -> ( n ` (/) ) = ( i ` (/) ) )
225 224 opeq2d 
 |-  ( n = i -> <. X , ( n ` (/) ) >. = <. X , ( i ` (/) ) >. )
226 225 sneqd 
 |-  ( n = i -> { <. X , ( n ` (/) ) >. } = { <. X , ( i ` (/) ) >. } )
227 226 fveq2d 
 |-  ( n = i -> ( F ` { <. X , ( n ` (/) ) >. } ) = ( F ` { <. X , ( i ` (/) ) >. } ) )
228 fveq1 
 |-  ( f = F -> ( f ` { <. X , ( n ` (/) ) >. } ) = ( F ` { <. X , ( n ` (/) ) >. } ) )
229 228 mpteq2dv 
 |-  ( f = F -> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
230 ovexd 
 |-  ( ph -> ( NN0 ^m 1o ) e. _V )
231 230 mptexd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) e. _V )
232 6 229 9 231 fvmptd3 
 |-  ( ph -> ( M ` F ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
233 232 adantr 
 |-  ( ( ph /\ i e. ( NN0 ^m 1o ) ) -> ( M ` F ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
234 simpr 
 |-  ( ( ph /\ i e. ( NN0 ^m 1o ) ) -> i e. ( NN0 ^m 1o ) )
235 fvexd 
 |-  ( ( ph /\ i e. ( NN0 ^m 1o ) ) -> ( F ` { <. X , ( i ` (/) ) >. } ) e. _V )
236 227 233 234 235 fvmptd4 
 |-  ( ( ph /\ i e. ( NN0 ^m 1o ) ) -> ( ( M ` F ) ` i ) = ( F ` { <. X , ( i ` (/) ) >. } ) )
237 223 236 syldan 
 |-  ( ( ph /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( M ` F ) ` i ) = ( F ` { <. X , ( i ` (/) ) >. } ) )
238 237 adantlr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( M ` F ) ` i ) = ( F ` { <. X , ( i ` (/) ) >. } ) )
239 fveq1 
 |-  ( f = G -> ( f ` { <. X , ( n ` (/) ) >. } ) = ( G ` { <. X , ( n ` (/) ) >. } ) )
240 239 mpteq2dv 
 |-  ( f = G -> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( n ` (/) ) >. } ) ) )
241 230 mptexd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( n ` (/) ) >. } ) ) e. _V )
242 6 240 10 241 fvmptd3 
 |-  ( ph -> ( M ` G ) = ( n e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( n ` (/) ) >. } ) ) )
243 fveq1 
 |-  ( n = m -> ( n ` (/) ) = ( m ` (/) ) )
244 243 opeq2d 
 |-  ( n = m -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
245 244 sneqd 
 |-  ( n = m -> { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } )
246 245 fveq2d 
 |-  ( n = m -> ( G ` { <. X , ( n ` (/) ) >. } ) = ( G ` { <. X , ( m ` (/) ) >. } ) )
247 246 cbvmptv 
 |-  ( n e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( n ` (/) ) >. } ) ) = ( m e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( m ` (/) ) >. } ) )
248 242 247 eqtrdi 
 |-  ( ph -> ( M ` G ) = ( m e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( m ` (/) ) >. } ) ) )
249 248 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( M ` G ) = ( m e. ( NN0 ^m 1o ) |-> ( G ` { <. X , ( m ` (/) ) >. } ) ) )
250 simpr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> m = ( n oF - i ) )
251 250 fveq1d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( m ` (/) ) = ( ( n oF - i ) ` (/) ) )
252 54 a1i 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> (/) e. 1o )
253 118 adantl 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n Fn 1o )
254 253 ad2antrr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> n Fn 1o )
255 102 116 syl 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i Fn 1o )
256 255 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> i Fn 1o )
257 50 a1i 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> 1o e. _V )
258 eqidd 
 |-  ( ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) /\ (/) e. 1o ) -> ( n ` (/) ) = ( n ` (/) ) )
259 eqidd 
 |-  ( ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) /\ (/) e. 1o ) -> ( i ` (/) ) = ( i ` (/) ) )
260 254 256 257 257 121 258 259 ofval 
 |-  ( ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) /\ (/) e. 1o ) -> ( ( n oF - i ) ` (/) ) = ( ( n ` (/) ) - ( i ` (/) ) ) )
261 252 260 mpdan 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( ( n oF - i ) ` (/) ) = ( ( n ` (/) ) - ( i ` (/) ) ) )
262 251 261 eqtrd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( m ` (/) ) = ( ( n ` (/) ) - ( i ` (/) ) ) )
263 98 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> X e. V )
264 fvexd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( m ` (/) ) e. _V )
265 fvsng 
 |-  ( ( X e. V /\ ( m ` (/) ) e. _V ) -> ( { <. X , ( m ` (/) ) >. } ` X ) = ( m ` (/) ) )
266 263 264 265 syl2anc 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( { <. X , ( m ` (/) ) >. } ` X ) = ( m ` (/) ) )
267 263 154 syl 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> X e. { X } )
268 129 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> { <. X , ( n ` (/) ) >. } Fn { X } )
269 127 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> { <. X , ( i ` (/) ) >. } Fn { X } )
270 47 a1i 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> { X } e. _V )
271 141 ad2antrr 
 |-  ( ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) /\ X e. { X } ) -> ( { <. X , ( n ` (/) ) >. } ` X ) = ( n ` (/) ) )
272 135 ad2antrr 
 |-  ( ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) /\ X e. { X } ) -> ( { <. X , ( i ` (/) ) >. } ` X ) = ( i ` (/) ) )
273 268 269 270 270 130 271 272 ofval 
 |-  ( ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) /\ X e. { X } ) -> ( ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ` X ) = ( ( n ` (/) ) - ( i ` (/) ) ) )
274 267 273 mpdan 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ` X ) = ( ( n ` (/) ) - ( i ` (/) ) ) )
275 262 266 274 3eqtr4d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( { <. X , ( m ` (/) ) >. } ` X ) = ( ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ` X ) )
276 elsni 
 |-  ( x e. { ( n ` (/) ) } -> x = ( n ` (/) ) )
277 276 adantr 
 |-  ( ( x e. { ( n ` (/) ) } /\ y e. ( 0 ... ( n ` (/) ) ) ) -> x = ( n ` (/) ) )
278 277 oveq1d 
 |-  ( ( x e. { ( n ` (/) ) } /\ y e. ( 0 ... ( n ` (/) ) ) ) -> ( x - y ) = ( ( n ` (/) ) - y ) )
279 fznn0sub2 
 |-  ( y e. ( 0 ... ( n ` (/) ) ) -> ( ( n ` (/) ) - y ) e. ( 0 ... ( n ` (/) ) ) )
280 279 adantl 
 |-  ( ( x e. { ( n ` (/) ) } /\ y e. ( 0 ... ( n ` (/) ) ) ) -> ( ( n ` (/) ) - y ) e. ( 0 ... ( n ` (/) ) ) )
281 278 280 eqeltrd 
 |-  ( ( x e. { ( n ` (/) ) } /\ y e. ( 0 ... ( n ` (/) ) ) ) -> ( x - y ) e. ( 0 ... ( n ` (/) ) ) )
282 281 adantl 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ ( x e. { ( n ` (/) ) } /\ y e. ( 0 ... ( n ` (/) ) ) ) ) -> ( x - y ) e. ( 0 ... ( n ` (/) ) ) )
283 fvex 
 |-  ( n ` (/) ) e. _V
284 152 283 f1osn 
 |-  { <. (/) , ( n ` (/) ) >. } : { (/) } -1-1-onto-> { ( n ` (/) ) }
285 f1of 
 |-  ( { <. (/) , ( n ` (/) ) >. } : { (/) } -1-1-onto-> { ( n ` (/) ) } -> { <. (/) , ( n ` (/) ) >. } : { (/) } --> { ( n ` (/) ) } )
286 284 285 mp1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. (/) , ( n ` (/) ) >. } : { (/) } --> { ( n ` (/) ) } )
287 fvsng 
 |-  ( ( (/) e. _V /\ ( n ` (/) ) e. NN0 ) -> ( { <. (/) , ( n ` (/) ) >. } ` (/) ) = ( n ` (/) ) )
288 152 56 287 sylancr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( { <. (/) , ( n ` (/) ) >. } ` (/) ) = ( n ` (/) ) )
289 288 eqcomd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) = ( { <. (/) , ( n ` (/) ) >. } ` (/) ) )
290 152 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> (/) e. _V )
291 150 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { (/) } = 1o )
292 55 56 fsnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. (/) , ( n ` (/) ) >. } : { (/) } --> NN0 )
293 291 292 feq2dd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. (/) , ( n ` (/) ) >. } : 1o --> NN0 )
294 293 ffnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. (/) , ( n ` (/) ) >. } Fn 1o )
295 290 149 253 294 fsneq 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n = { <. (/) , ( n ` (/) ) >. } <-> ( n ` (/) ) = ( { <. (/) , ( n ` (/) ) >. } ` (/) ) ) )
296 289 295 mpbird 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n = { <. (/) , ( n ` (/) ) >. } )
297 149 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 1o = { (/) } )
298 296 297 feq12d 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n : 1o --> { ( n ` (/) ) } <-> { <. (/) , ( n ` (/) ) >. } : { (/) } --> { ( n ` (/) ) } ) )
299 286 298 mpbird 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> { ( n ` (/) ) } )
300 299 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> n : 1o --> { ( n ` (/) ) } )
301 149 fneq2i 
 |-  ( i Fn 1o <-> i Fn { (/) } )
302 255 301 sylib 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i Fn { (/) } )
303 0zd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> 0 e. ZZ )
304 139 nn0zd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( n ` (/) ) e. ZZ )
305 105 nn0zd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( i ` (/) ) e. ZZ )
306 105 nn0ge0d 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> 0 <_ ( i ` (/) ) )
307 303 304 305 306 125 elfzd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( i ` (/) ) e. ( 0 ... ( n ` (/) ) ) )
308 fveq2 
 |-  ( o = (/) -> ( i ` o ) = ( i ` (/) ) )
309 308 eleq1d 
 |-  ( o = (/) -> ( ( i ` o ) e. ( 0 ... ( n ` (/) ) ) <-> ( i ` (/) ) e. ( 0 ... ( n ` (/) ) ) ) )
310 152 309 ralsn 
 |-  ( A. o e. { (/) } ( i ` o ) e. ( 0 ... ( n ` (/) ) ) <-> ( i ` (/) ) e. ( 0 ... ( n ` (/) ) ) )
311 307 310 sylibr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> A. o e. { (/) } ( i ` o ) e. ( 0 ... ( n ` (/) ) ) )
312 ffnfv 
 |-  ( i : { (/) } --> ( 0 ... ( n ` (/) ) ) <-> ( i Fn { (/) } /\ A. o e. { (/) } ( i ` o ) e. ( 0 ... ( n ` (/) ) ) ) )
313 302 311 312 sylanbrc 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> i : { (/) } --> ( 0 ... ( n ` (/) ) ) )
314 149 99 eqeltrrid 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> { (/) } e. _V )
315 149 ineq2i 
 |-  ( 1o i^i 1o ) = ( 1o i^i { (/) } )
316 315 121 eqtr3i 
 |-  ( 1o i^i { (/) } ) = 1o
317 282 300 313 99 314 316 off 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( n oF - i ) : 1o --> ( 0 ... ( n ` (/) ) ) )
318 fz0ssnn0 
 |-  ( 0 ... ( n ` (/) ) ) C_ NN0
319 318 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( 0 ... ( n ` (/) ) ) C_ NN0 )
320 317 319 fssd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( n oF - i ) : 1o --> NN0 )
321 320 adantr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( n oF - i ) : 1o --> NN0 )
322 321 252 ffvelcdmd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( ( n oF - i ) ` (/) ) e. NN0 )
323 251 322 eqeltrd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( m ` (/) ) e. NN0 )
324 263 323 fsnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> { <. X , ( m ` (/) ) >. } : { X } --> NN0 )
325 324 ffnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> { <. X , ( m ` (/) ) >. } Fn { X } )
326 268 269 270 270 130 offn 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) Fn { X } )
327 263 209 325 326 fsneq 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( { <. X , ( m ` (/) ) >. } = ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) <-> ( { <. X , ( m ` (/) ) >. } ` X ) = ( ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ` X ) ) )
328 275 327 mpbird 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> { <. X , ( m ` (/) ) >. } = ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) )
329 328 fveq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) /\ m = ( n oF - i ) ) -> ( G ` { <. X , ( m ` (/) ) >. } ) = ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) )
330 96 99 320 elmapdd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( n oF - i ) e. ( NN0 ^m 1o ) )
331 fvexd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) e. _V )
332 249 329 330 331 fvmptd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( M ` G ) ` ( n oF - i ) ) = ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) )
333 238 332 oveq12d 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } ) -> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) = ( ( F ` { <. X , ( i ` (/) ) >. } ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) ) )
334 333 mpteq2dva 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) = ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( F ` { <. X , ( i ` (/) ) >. } ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) ) ) )
335 334 oveq2d 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) = ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( F ` { <. X , ( i ` (/) ) >. } ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - { <. X , ( i ` (/) ) >. } ) ) ) ) ) )
336 221 335 eqtr4d 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ { <. X , ( n ` (/) ) >. } } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( { <. X , ( n ` (/) ) >. } oF - j ) ) ) ) ) = ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) )
337 23 336 sylan9eqr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m = { <. X , ( n ` (/) ) >. } ) -> ( R gsum ( j e. { l e. { g e. ( NN0 ^m { X } ) | g finSupp 0 } | l oR <_ m } |-> ( ( F ` j ) ( .r ` R ) ( G ` ( m oF - j ) ) ) ) ) = ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) )
338 ovexd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) e. _V )
339 17 337 64 338 fvmptd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( F .x. G ) ` { <. X , ( n ` (/) ) >. } ) = ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) )
340 339 mpteq2dva 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( F .x. G ) ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) ) )
341 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
342 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
343 5 342 ply1bas 
 |-  ( Base ` Q ) = ( Base ` ( 1o mPoly R ) )
344 5 341 4 ply1mulr 
 |-  .X. = ( .r ` ( 1o mPoly R ) )
345 psr1baslem 
 |-  ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
346 1 2 3 4 5 6 7 8 9 selvply1rhmlema 
 |-  ( ph -> ( M ` F ) e. ( Base ` Q ) )
347 1 2 3 4 5 6 7 8 10 selvply1rhmlema 
 |-  ( ph -> ( M ` G ) e. ( Base ` Q ) )
348 341 343 13 344 345 346 347 mplmul 
 |-  ( ph -> ( ( M ` F ) .X. ( M ` G ) ) = ( n e. ( NN0 ^m 1o ) |-> ( R gsum ( i e. { k e. ( NN0 ^m 1o ) | k oR <_ n } |-> ( ( ( M ` F ) ` i ) ( .r ` R ) ( ( M ` G ) ` ( n oF - i ) ) ) ) ) ) )
349 340 348 eqtr4d 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( F .x. G ) ` { <. X , ( n ` (/) ) >. } ) ) = ( ( M ` F ) .X. ( M ` G ) ) )
350 12 349 sylan9eqr 
 |-  ( ( ph /\ f = ( F .x. G ) ) -> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) = ( ( M ` F ) .X. ( M ` G ) ) )
351 47 a1i 
 |-  ( ph -> { X } e. _V )
352 2 351 8 mplringd 
 |-  ( ph -> P e. Ring )
353 1 3 352 9 10 ringcld 
 |-  ( ph -> ( F .x. G ) e. B )
354 ovexd 
 |-  ( ph -> ( ( M ` F ) .X. ( M ` G ) ) e. _V )
355 6 350 353 354 fvmptd2 
 |-  ( ph -> ( M ` ( F .x. G ) ) = ( ( M ` F ) .X. ( M ` G ) ) )