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